1 /-
2 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Jeremy Avigad, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
5
6 -- QUESTION: can make the first argument in ∀ x ∈ a, ... implicit?
7 -/
8 import logic.basic data.set.basic data.equiv.basic
src └─────────┘ └────────────┘ └──────────────┘
9 import order.complete_boolean_algebra category.basic
src └────────────────────────────┘ └────────────┘
10 import tactic.finish data.sigma.basic order.galois_connection
src └───────────┘ └──────────────┘ └─────────────────────┘
11
12 open function tactic set lattice auto
13
14 universes u v w x y
15 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {ι' : Sort y}
16
17 namespace set
18
19 instance lattice_set : complete_lattice (set α) :=
id └──────────────┘ └─┘ ┴
src └──────────────┘ └─┘
typ └──────────────┘ └─┘ ┴
doc └──────────────┘
20 { le := (⊆),
id ┴
src ┴
typ ┴
21 lt := (⊂),
id ┴
src ┴
typ ┴
22 sup := (∪),
id ┴
src ┴
typ ┴
23 inf := (∩),
id ┴
src ┴
typ ┴
24 top := univ,
id └──┘
src └──┘
typ └──┘
25 bot := ∅,
id ┴
src ┴
typ ┴
26 Sup := λs, {a | ∃ t ∈ s, a ∈ t },
id ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴
27 Inf := λs, {a | ∀ t ∈ s, a ∈ t },
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
28
29 le_Sup := assume s t t_in a a_in, ⟨t, ⟨t_in, a_in⟩⟩,
id ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ └──┘
typ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ └──┘
30 Sup_le := assume s t h a ⟨t', ⟨t'_in, a_in⟩⟩, h t' t'_in a_in,
id ┴ ┴ ┴ ┴ ┴└┘ └───┘ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴└┘ └───┘ └──┘ ┴
31
32 le_Inf := assume s t h a a_in t' t'_in, h t' t'_in a_in,
id ┴ ┴ ┴ ┴ └──┘ └┘ └───┘ ┴ └┘ └───┘ └──┘
typ ┴ ┴ ┴ ┴ └──┘ └┘ └───┘ ┴ └┘ └───┘ └──┘
33 Inf_le := assume s t t_in a h, h _ t_in,
id ┴ ┴ └──┘ ┴ ┴ ┴ └──┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘
34 .. (infer_instance : complete_lattice (α → Prop)) }
id └────────────┘ └──────────────┘ ┴
src └────────────┘ └──────────────┘
typ └────────────┘ └──────────────┘ ┴
doc └────────────┘ └──────────────┘
35
36 instance : distrib_lattice (set α) :=
id └─────────────┘ └─┘ ┴
src └─────────────┘ └─┘
typ └─────────────┘ └─┘ ┴
doc └─────────────┘
37 { le_sup_inf := λ s t u x, or_and_distrib_left.2, ..set.lattice_set }
id ┴ ┴ ┴ ┴ └─────────────────┘┴ └─────────────┘
src └─────────────────┘┴ └─────────────┘
typ ┴ ┴ ┴ ┴ └─────────────────┘┴ └─────────────┘
38
39 lemma monotone_image {f : α → β} : monotone (image f) :=
id ┴ ┴ └──────┘ └───┘ ┴
src └──────┘ └───┘
typ ┴ ┴ └──────┘ └───┘ ┴
doc └──────┘
40 assume s t, assume h : s ⊆ t, image_subset _ h
id ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
src ┴ └──────────┘
typ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
41
42 theorem monotone_inter [preorder β] {f g : β → set α}
id └──────┘ ┴ ┴ └─┘ ┴
src └──────┘ └─┘
typ └──────┘ ┴ ┴ └─┘ ┴
43 (hf : monotone f) (hg : monotone g) : monotone (λx, f x ∩ g x) :=
id └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘
44 assume b₁ b₂ h, inter_subset_inter (hf h) (hg h)
id └┘ └┘ ┴ └────────────────┘ └┘ ┴ └┘ ┴
src └────────────────┘
typ └┘ └┘ ┴ └────────────────┘ └┘ ┴ └┘ ┴
45
46 theorem monotone_union [preorder β] {f g : β → set α}
id └──────┘ ┴ ┴ └─┘ ┴
src └──────┘ └─┘
typ └──────┘ ┴ ┴ └─┘ ┴
47 (hf : monotone f) (hg : monotone g) : monotone (λx, f x ∪ g x) :=
id └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘
48 assume b₁ b₂ h, union_subset_union (hf h) (hg h)
id └┘ └┘ ┴ └────────────────┘ └┘ ┴ └┘ ┴
src └────────────────┘
typ └┘ └┘ ┴ └────────────────┘ └┘ ┴ └┘ ┴
49
50 theorem monotone_set_of [preorder α] {p : α → β → Prop}
id └──────┘ ┴ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴ ┴
51 (hp : ∀b, monotone (λa, p a b)) : monotone (λa, {b | p a b}) :=
id ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴┴ ┴ ┴ ┴
src └──────┘ └──────┘ ┴
typ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴┴ ┴ ┴ ┴
doc └──────┘ └──────┘
52 assume a a' h b, hp b h
id ┴ └┘ ┴ ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴
53
54 section galois_connection
55 variables {f : α → β}
56
57 protected lemma image_preimage : galois_connection (image f) (preimage f) :=
id └───────────────┘ └───┘ ┴ └──────┘ ┴
src └───────────────┘ └───┘ └──────┘
typ └───────────────┘ └───┘ ┴ └──────┘ ┴
doc └───────────────┘ └──────┘
58 assume a b, image_subset_iff
id ┴ ┴ └──────────────┘
src └──────────────┘
typ ┴ ┴ └──────────────┘
doc └──────────────┘
59
60 def kern_image (f : α → β) (s : set α) : set β := {y | ∀x, f x = y → x ∈ s}
id ┴ ┴ └─┘ ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
61
62 protected lemma preimage_kern_image : galois_connection (preimage f) (kern_image f) :=
id └───────────────┘ └──────┘ ┴ └────────┘ ┴
src └───────────────┘ └──────┘ └────────┘
typ └───────────────┘ └──────┘ ┴ └────────┘ ┴
doc └───────────────┘ └──────┘
63 assume a b,
id ┴ ┴
typ ┴ ┴
64 ⟨ assume h x hx y hy, have f y ∈ a, from hy.symm ▸ hx, h this,
id ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘└───┘ ┴ └┘ ┴ └──┘
src ┴ └───┘ ┴
typ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘└───┘ ┴ └┘ ┴ └──┘
65 assume h x (hx : f x ∈ a), h hx x rfl⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
src ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
66
67 end galois_connection
68
69 /- union and intersection over a family of sets indexed by a type -/
70
71 /-- Indexed union of a family of sets -/
72 @[reducible] def Union (s : ι → set β) : set β := supr s
id ┴ └─┘ ┴ └─┘ ┴ └──┘ ┴
src └─┘ └─┘ └──┘
typ ┴ └─┘ ┴ └─┘ ┴ └──┘ ┴
doc └───────┘ └──┘
73
74 /-- Indexed intersection of a family of sets -/
75 @[reducible] def Inter (s : ι → set β) : set β := infi s
id ┴ └─┘ ┴ └─┘ ┴ └──┘ ┴
src └─┘ └─┘ └──┘
typ ┴ └─┘ ┴ └─┘ ┴ └──┘ ┴
doc └───────┘ └──┘
76
77 notation `⋃` binders `, ` r:(scoped f, Union f) := r
id └───┘
src └───┘
typ └───┘
doc └───┘
78 notation `⋂` binders `, ` r:(scoped f, Inter f) := r
id └───┘
src └───┘
typ └───┘
doc └───┘
79
80 @[simp] theorem mem_Union {x : β} {s : ι → set β} : x ∈ Union s ↔ ∃ i, x ∈ s i :=
id ┴ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──┘ └───┘
81 ⟨assume ⟨t, ⟨⟨a, (t_eq : s a = t)⟩, (h : x ∈ t)⟩⟩, ⟨a, t_eq.symm ▸ h⟩,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
src ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
82 assume ⟨a, h⟩, ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩
id ┴┴ ┴ ┴ └─┘
src └─┘
typ ┴┴ ┴ ┴ └─┘
83 /- alternative proof: dsimp [Union, supr, Sup]; simp -/
84 -- TODO: more rewrite rules wrt forall / existentials and logical connectives
85 -- TODO: also eliminate ∃i, ... ∧ i = t ∧ ...
86
87 @[simp] theorem mem_Inter {x : β} {s : ι → set β} : x ∈ Inter s ↔ ∀ i, x ∈ s i :=
id ┴ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └───┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───┘
88 ⟨assume (h : ∀a ∈ {a : set β | ∃i, s i = a}, x ∈ a) a, h (s a) ⟨a, rfl⟩,
id ┴ ┴ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ └─┘ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
89 assume h t ⟨a, (eq : s a = t)⟩, eq ▸ h a⟩
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
90
91 theorem Union_subset {s : ι → set β} {t : set β} (h : ∀ i, s i ⊆ t) : (⋃ i, s i) ⊆ t :=
id ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴
92 -- TODO: should be simpler when sets' order is based on lattices
93 @supr_le (set β) _ set.lattice_set _ _ h
id └─────┘ └─┘ ┴ └─────────────┘ ┴
src └─────┘ └─┘ └─────────────┘
typ └─────┘ └─┘ ┴ └─────────────┘ ┴
94
95 theorem Union_subset_iff {s : ι → set β} {t : set β} : (⋃ i, s i) ⊆ t ↔ (∀ i, s i ⊆ t) :=
id ┴ └─┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
96 ⟨assume h i, subset.trans (le_supr s _) h, Union_subset⟩
id ┴ ┴ └──────────┘ └─────┘ ┴ ┴ └──────────┘
src └──────────┘ └─────┘ └──────────┘
typ ┴ ┴ └──────────┘ └─────┘ ┴ ┴ └──────────┘
97
98 theorem mem_Inter_of_mem {x : β} {s : ι → set β} : (∀ i, x ∈ s i) → (x ∈ ⋂ i, s i) :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
99 mem_Inter.2
id └───────┘┴
src └───────┘┴
typ └───────┘┴
100
101 theorem subset_Inter {t : set β} {s : ι → set β} (h : ∀ i, t ⊆ s i) : t ⊆ ⋂ i, s i :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
102 -- TODO: should be simpler when sets' order is based on lattices
103 @le_infi (set β) _ set.lattice_set _ _ h
id └─────┘ └─┘ ┴ └─────────────┘ ┴
src └─────┘ └─┘ └─────────────┘
typ └─────┘ └─┘ ┴ └─────────────┘ ┴
104
105 theorem subset_Union : ∀ (s : ι → set β) (i : ι), s i ⊆ (⋃ i, s i) := le_supr
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘
src └─┘ ┴ ┴ ┴ └─────┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘
doc ┴ ┴
106
107 theorem Inter_subset : ∀ (s : ι → set β) (i : ι), (⋂ i, s i) ⊆ s i := infi_le
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─┘ ┴ ┴ ┴ └─────┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc ┴ ┴
108
109 lemma Inter_subset_of_subset {s : ι → set α} {t : set α} (i : ι)
id ┴ └─┘ ┴ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ └─┘ ┴ ┴
110 (h : s i ⊆ t) : (⋂ i, s i) ⊆ t :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴
111 set.subset.trans (set.Inter_subset s i) h
id └──────────────┘ └──────────────┘ ┴ ┴ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ └──────────────┘ ┴ ┴ ┴
112
113 lemma Inter_subset_Inter {s t : ι → set α} (h : ∀ i, s i ⊆ t i) :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
114 (⋂ i, s i) ⊆ (⋂ i, t i) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
115 set.subset_Inter $ λ i, set.Inter_subset_of_subset i (h i)
id └──────────────┘ ┴ └────────────────────────┘ ┴ ┴ ┴
src └──────────────┘ └────────────────────────┘
typ └──────────────┘ ┴ └────────────────────────┘ ┴ ┴ ┴
116
117 lemma Inter_subset_Inter2 {s : ι → set α} {t : ι' → set α} (h : ∀ j, ∃ i, s i ⊆ t j) :
id ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
118 (⋂ i, s i) ⊆ (⋂ j, t j) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
119 set.subset_Inter $ λ j, let ⟨i, hi⟩ := h j in Inter_subset_of_subset i hi
id └──────────────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └────────────────────┘
src └──────────────┘ └────────────────────┘
typ └──────────────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └────────────────────┘
120
121 theorem Union_const [inhabited ι] (s : set β) : (⋃ i:ι, s) = s :=
id └───────┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ ┴
typ └───────┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴
122 ext $ by simp
id └─┘
src └─┘ └────
typ └─┘ └────
doc └────
txt └────
par └────
pid └
st └─────
123
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
124 theorem Inter_const [inhabited ι] (s : set β) : (⋂ i:ι, s) = s :=
id └───────┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ ┴
typ └───────┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴
125 ext $ by simp
id └─┘
src └─┘ └────
typ └─┘ └────
doc └────
txt └────
par └────
pid └
st └─────
126
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
127 @[simp] -- complete_boolean_algebra
doc └──┘
128 theorem compl_Union (s : ι → set β) : - (⋃ i, s i) = (⋂ i, - s i) :=
id ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
129 ext (by simp)
id └─┘
src └─┘ └──┘
typ └─┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
130
131 -- classical -- complete_boolean_algebra
132 theorem compl_Inter (s : ι → set β) : -(⋂ i, s i) = (⋃ i, - s i) :=
id ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
133 ext (λ x, by simp [classical.not_forall])
id └─┘ ┴ └──────────────────┘
src └─┘ └────┘└──────────────────┘┴
typ └─┘ ┴ └────┘└──────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └──────────────────────────┘
134
135 -- classical -- complete_boolean_algebra
136 theorem Union_eq_comp_Inter_comp (s : ι → set β) : (⋃ i, s i) = - (⋂ i, - s i) :=
id ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
137 by simp [compl_Inter, compl_compl]
id └─────────┘ └─────────┘
src └────┘└─────────┘└┘└─────────┘└─
typ └────┘└─────────┘└┘└─────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────────
138
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
139 -- classical -- complete_boolean_algebra
src ────────────────────────────────────────┘
typ ────────────────────────────────────────┘
doc ────────────────────────────────────────┘
txt ────────────────────────────────────────┘
par ────────────────────────────────────────┘
pid ────────────────────────────────────────┘
st ────────────────────────────────────────┘
140 theorem Inter_eq_comp_Union_comp (s : ι → set β) : (⋂ i, s i) = - (⋃ i, -s i) :=
id ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴
doc ┴ ┴ ┴ ┴
141 by simp [compl_compl]
id └─────────┘
src └────┘└─────────┘└─
typ └────┘└─────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────
142
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
143 theorem inter_Union (s : set β) (t : ι → set β) :
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
144 s ∩ (⋃ i, t i) = ⋃ i, s ∩ t i :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
145 ext $ by simp
id └─┘
src └─┘ └────
typ └─┘ └────
doc └────
txt └────
par └────
pid └
st └─────
146
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
147 theorem Union_inter (s : set β) (t : ι → set β) :
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
148 (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
149 ext $ by simp
id └─┘
src └─┘ └────
typ └─┘ └────
doc └────
txt └────
par └────
pid └
st └─────
150
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
151 theorem Union_union_distrib (s : ι → set β) (t : ι → set β) :
id ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ ┴ └─┘ ┴
152 (⋃ i, s i ∪ t i) = (⋃ i, s i) ∪ (⋃ i, t i) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
153 ext $ by simp [exists_or_distrib]
id └─┘ └───────────────┘
src └─┘ └────┘└───────────────┘└─
typ └─┘ └────┘└───────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────────────────────
154
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
155 theorem Inter_inter_distrib (s : ι → set β) (t : ι → set β) :
id ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ ┴ └─┘ ┴
156 (⋂ i, s i ∩ t i) = (⋂ i, s i) ∩ (⋂ i, t i) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
157 ext $ by simp [forall_and_distrib]
id └─┘ └────────────────┘
src └─┘ └────┘└────────────────┘└─
typ └─┘ └────┘└────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────────
158
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
159 theorem union_Union [inhabited ι] (s : set β) (t : ι → set β) :
id └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘ └─┘
typ └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
160 s ∪ (⋃ i, t i) = ⋃ i, s ∪ t i :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
161 by rw [Union_union_distrib, Union_const]
id └─────────────────┘ └─────────┘
src └──┘└─────────────────┘└┘└─────────┘└─
typ └──┘└─────────────────┘└┘└─────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────────────┘└───────────┘┴└
162
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
163 theorem Union_union [inhabited ι] (s : set β) (t : ι → set β) :
id └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘ └─┘
typ └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
164 (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
165 by rw [Union_union_distrib, Union_const]
id └─────────────────┘ └─────────┘
src └──┘└─────────────────┘└┘└─────────┘└─
typ └──┘└─────────────────┘└┘└─────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────────────┘└───────────┘┴└
166
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
167 theorem inter_Inter [inhabited ι] (s : set β) (t : ι → set β) :
id └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘ └─┘
typ └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
168 s ∩ (⋂ i, t i) = ⋂ i, s ∩ t i :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
169 by rw [Inter_inter_distrib, Inter_const]
id └─────────────────┘ └─────────┘
src └──┘└─────────────────┘└┘└─────────┘└─
typ └──┘└─────────────────┘└┘└─────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────────────┘└───────────┘┴└
170
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
171 theorem Inter_inter [inhabited ι] (s : set β) (t : ι → set β) :
id └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘ └─┘
typ └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
172 (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
173 by rw [Inter_inter_distrib, Inter_const]
id └─────────────────┘ └─────────┘
src └──┘└─────────────────┘└┘└─────────┘└─
typ └──┘└─────────────────┘└┘└─────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────────────────┘└───────────┘┴└
174
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
175 -- classical
src ────────────┘
typ ────────────┘
doc ────────────┘
txt ────────────┘
par ────────────┘
pid ────────────┘
st ────────────┘
176 theorem union_Inter (s : set β) (t : ι → set β) :
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
177 s ∪ (⋂ i, t i) = ⋂ i, s ∪ t i :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
178 ext $ assume x, by simp [classical.forall_or_distrib_left]
id └─┘ ┴ └──────────────────────────────┘
src └─┘ └────┘└──────────────────────────────┘└─
typ └─┘ ┴ └────┘└──────────────────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────────────────────────
179
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
180 theorem Union_diff (s : set β) (t : ι → set β) :
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
181 (⋃ i, t i) \ s = ⋃ i, t i \ s :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
182 Union_inter _ _
id └─────────┘
src └─────────┘
typ └─────────┘
183
184 theorem diff_Union [inhabited ι] (s : set β) (t : ι → set β) :
id └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────┘ └─┘ └─┘
typ └───────┘ ┴ └─┘ ┴ ┴ └─┘ ┴
185 s \ (⋃ i, t i) = ⋂ i, s \ t i :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
186 by rw [diff_eq, compl_Union, inter_Inter]; refl
id └─────┘ └─────────┘ └─────────┘
src └──┘└─────┘└┘└─────────┘└┘└─────────┘┴ └────
typ └──┘└─────┘└┘└─────────┘└┘└─────────┘┴ └────
doc └──┘ └┘ └┘ ┴ └────
txt └──┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ ┴ └
st └──────────┘└───────────┘└───────────┘┴└──────
187
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
188 theorem diff_Inter (s : set β) (t : ι → set β) :
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
189 s \ (⋂ i, t i) = ⋃ i, s \ t i :=
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
190 by rw [diff_eq, compl_Inter, inter_Union]; refl
id └─────┘ └─────────┘ └─────────┘
src └──┘└─────┘└┘└─────────┘└┘└─────────┘┴ └────
typ └──┘└─────┘└┘└─────────┘└┘└─────────┘┴ └────
doc └──┘ └┘ └┘ ┴ └────
txt └──┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ ┴ └
st └──────────┘└───────────┘└───────────┘┴└──────
191
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
192 /- bounded unions and intersections -/
src ───────────────────────────────────────
typ ───────────────────────────────────────
doc ───────────────────────────────────────
txt ───────────────────────────────────────
par ───────────────────────────────────────
pid ───────────────────────────────────────
st ───────────────────────────────────────
193
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
194 theorem mem_bUnion_iff {s : set α} {t : α → set β} {y : β} :
id └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴
195 y ∈ (⋃ x ∈ s, t x) ↔ ∃ x ∈ s, y ∈ t x := by simp
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └────
doc ┴ ┴ └────
txt └────
par └────
pid └
st └─────
196
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
197 theorem mem_bInter_iff {s : set α} {t : α → set β} {y : β} :
id └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴
198 y ∈ (⋂ x ∈ s, t x) ↔ ∀ x ∈ s, y ∈ t x := by simp
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └────
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
doc ┴ ┴ └────
txt └────
par └────
pid └
st └─────
199
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
200 theorem mem_bUnion {s : set α} {t : α → set β} {x : α} {y : β} (xs : x ∈ s) (ytx : y ∈ t x) :
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
201 y ∈ ⋃ x ∈ s, t x :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
202 by simp; exact ⟨x, ⟨xs, ytx⟩⟩
id ┴ └┘ └─┘
src └──┘ └────┘ └┘ └┘ └──
typ └──┘ └────┘ ┴└┘ └┘└┘└─┘└──
doc └──┘ └────┘ └┘ └┘ └──
txt └──┘ └────┘ └┘ └┘ └──
par └──┘ └────┘ └┘ └┘ └──
pid ┴ └┘ └┘ └┘└
st └───────────────────────────
203
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
204 theorem mem_bInter {s : set α} {t : α → set β} {y : β} (h : ∀ x ∈ s, y ∈ t x) :
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
205 y ∈ ⋂ x ∈ s, t x :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
206 by simp; assumption
src └──┘ └──────────
typ └──┘ └──────────
doc └──┘ └──────────
txt └──┘ └──────────
par └──┘ └──────────
pid └
st └─────────────────
207
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
208 theorem bUnion_subset {s : set α} {t : set β} {u : α → set β} (h : ∀ x ∈ s, u x ⊆ t) :
id └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └─┘ ┴
typ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
209 (⋃ x ∈ s, u x) ⊆ t :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴
210 show (⨆ x ∈ s, u x) ≤ t, -- TODO: should not be necessary when sets' order is based on lattices
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴
211 from supr_le $ assume x, supr_le (h x)
id └─────┘ ┴ └─────┘ ┴ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴
212
213 theorem subset_bInter {s : set α} {t : set β} {u : α → set β} (h : ∀ x ∈ s, t ⊆ u x) :
id └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └─┘ ┴
typ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
214 t ⊆ (⋂ x ∈ s, u x) :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
215 subset_Inter $ assume x, subset_Inter $ h x
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
216
217 theorem subset_bUnion_of_mem {s : set α} {u : α → set β} {x : α} (xs : x ∈ s) :
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
218 u x ⊆ (⋃ x ∈ s, u x) :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
219 show u x ≤ (⨆ x ∈ s, u x),
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴
220 from le_supr_of_le x $ le_supr _ xs
id └───────────┘ ┴ └─────┘ └┘
src └───────────┘ └─────┘
typ └───────────┘ ┴ └─────┘ └┘
221
222 theorem bInter_subset_of_mem {s : set α} {t : α → set β} {x : α} (xs : x ∈ s) :
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
223 (⋂ x ∈ s, t x) ⊆ t x :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
224 show (⨅x ∈ s, t x) ≤ t x,
id ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
225 from infi_le_of_le x $ infi_le _ xs
id └───────────┘ ┴ └─────┘ └┘
src └───────────┘ └─────┘
typ └───────────┘ ┴ └─────┘ └┘
226
227 theorem bUnion_subset_bUnion_left {s s' : set α} {t : α → set β}
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
228 (h : s ⊆ s') : (⋃ x ∈ s, t x) ⊆ (⋃ x ∈ s', t x) :=
id ┴ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴
doc ┴ ┴ ┴ ┴
229 bUnion_subset (λ x xs, subset_bUnion_of_mem (h xs))
id └───────────┘ ┴ └┘ └──────────────────┘ ┴ └┘
src └───────────┘ └──────────────────┘
typ └───────────┘ ┴ └┘ └──────────────────┘ ┴ └┘
230
231 theorem bInter_subset_bInter_left {s s' : set α} {t : α → set β}
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
232 (h : s' ⊆ s) : (⋂ x ∈ s, t x) ⊆ (⋂ x ∈ s', t x) :=
id └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘┴ ┴ ┴
doc ┴ ┴ ┴ ┴
233 subset_bInter (λ x xs, bInter_subset_of_mem (h xs))
id └───────────┘ ┴ └┘ └──────────────────┘ ┴ └┘
src └───────────┘ └──────────────────┘
typ └───────────┘ ┴ └┘ └──────────────────┘ ┴ └┘
234
235 theorem bUnion_subset_bUnion_right {s : set α} {t1 t2 : α → set β}
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
236 (h : ∀ x ∈ s, t1 x ⊆ t2 x) : (⋃ x ∈ s, t1 x) ⊆ (⋃ x ∈ s, t2 x) :=
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴
doc ┴ ┴ ┴ ┴
237 bUnion_subset (λ x xs, subset.trans (h x xs) (subset_bUnion_of_mem xs))
id └───────────┘ ┴ └┘ └──────────┘ ┴ ┴ └┘ └──────────────────┘ └┘
src └───────────┘ └──────────┘ └──────────────────┘
typ └───────────┘ ┴ └┘ └──────────┘ ┴ ┴ └┘ └──────────────────┘ └┘
238
239 theorem bInter_subset_bInter_right {s : set α} {t1 t2 : α → set β}
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
240 (h : ∀ x ∈ s, t1 x ⊆ t2 x) : (⋂ x ∈ s, t1 x) ⊆ (⋂ x ∈ s, t2 x) :=
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴┴ └┘ ┴
doc ┴ ┴ ┴ ┴
241 subset_bInter (λ x xs, subset.trans (bInter_subset_of_mem xs) (h x xs))
id └───────────┘ ┴ └┘ └──────────┘ └──────────────────┘ └┘ ┴ ┴ └┘
src └───────────┘ └──────────┘ └──────────────────┘
typ └───────────┘ ┴ └┘ └──────────┘ └──────────────────┘ └┘ ┴ ┴ └┘
242
243 theorem bUnion_eq_Union (s : set α) (t : α → set β) : (⋃ x ∈ s, t x) = (⋃ x : s, t x.1) :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc ┴ ┴ ┴ ┴
244 set.ext $ by simp
id └─────┘
src └─────┘ └────
typ └─────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
245
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
246 theorem bInter_eq_Inter (s : set α) (t : α → set β) : (⋂ x ∈ s, t x) = (⋂ x : s, t x.1) :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc ┴ ┴ ┴ ┴
247 set.ext $ by simp
id └─────┘
src └─────┘ └────
typ └─────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
248
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
249 @[simp] theorem bInter_empty (u : α → set β) : (⋂ x ∈ (∅ : set α), u x) = univ :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘
src └─┘ ┴ ┴ └─┘ ┴ ┴ └──┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘ ┴ ┴
250 show (⨅x ∈ (∅ : set α), u x) = ⊤, -- simplifier should be able to rewrite x ∈ ∅ to false.
id ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
251 from infi_emptyset
id └───────────┘
src └───────────┘
typ └───────────┘
252
253 @[simp] theorem bInter_univ (u : α → set β) : (⋂ x ∈ @univ α, u x) = ⋂ x, u x :=
id ┴ └─┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └─┘ ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴
254 infi_univ
id └───────┘
src └───────┘
typ └───────┘
255
256
257 -- TODO(Jeremy): here is an artifact of the the encoding of bounded intersection:
258 -- without dsimp, the next theorem fails to type check, because there is a lambda
259 -- in a type that needs to be contracted. Using simp [eq_of_mem_singleton xa] also works.
260
261 @[simp] theorem bInter_singleton (a : α) (s : α → set β) : (⋂ x ∈ ({a} : set α), s x) = s a :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
262 show (⨅ x ∈ ({a} : set α), s x) = s a, by simp
id ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴ └────
typ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
doc ┴ ┴ └────
txt └────
par └────
pid └
st └─────
263
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
264 theorem bInter_union (s t : set α) (u : α → set β) :
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
265 (⋂ x ∈ s ∪ t, u x) = (⋂ x ∈ s, u x) ∩ (⋂ x ∈ t, u x) :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
266 show (⨅ x ∈ s ∪ t, u x) = (⨅ x ∈ s, u x) ⊓ (⨅ x ∈ t, u x),
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
267 from infi_union
id └────────┘
src └────────┘
typ └────────┘
268
269 -- TODO(Jeremy): simp [insert_eq, bInter_union] doesn't work
270 @[simp] theorem bInter_insert (a : α) (s : set α) (t : α → set β) :
id ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └──┘
271 (⋂ x ∈ insert a s, t x) = t a ∩ (⋂ x ∈ s, t x) :=
id ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
272 begin rw insert_eq, simp [bInter_union] end
id └───────┘ └──────────┘
src └─┘└───────┘ └────┘└──────────┘└┘
typ └─┘└───────┘ └────┘└──────────┘└┘
doc └─┘ └────┘ └┘
txt └─┘ └────┘ └┘
par └─┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st └────────────────┘└────────────────────┘└─┘
273
274 -- TODO(Jeremy): another example of where an annotation is needed
275
276 theorem bInter_pair (a b : α) (s : α → set β) :
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
277 (⋂ x ∈ ({a, b} : set α), s x) = s a ∩ s b :=
id ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
278 by rw insert_of_has_insert; simp [inter_comm]
id └──────────────────┘ └────────┘
src └─┘└──────────────────┘ └────┘└────────┘└─
typ └─┘└──────────────────┘ └────┘└────────┘└─
doc └─┘ └────┘ └─
txt └─┘ └────┘ └─
par └─┘ └────┘ └─
pid ┴ ┴┴ ┴└
st └───────────────────────────────────────────
279
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
280 @[simp] theorem bUnion_empty (s : α → set β) : (⋃ x ∈ (∅ : set α), s x) = ∅ :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
281 supr_emptyset
id └───────────┘
src └───────────┘
typ └───────────┘
282
283 @[simp] theorem bUnion_univ (s : α → set β) : (⋃ x ∈ @univ α, s x) = ⋃ x, s x :=
id ┴ └─┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └─┘ ┴ └──┘ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴ ┴ ┴
284 supr_univ
id └───────┘
src └───────┘
typ └───────┘
285
286 @[simp] theorem bUnion_singleton (a : α) (s : α → set β) : (⋃ x ∈ ({a} : set α), s x) = s a :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
287 supr_singleton
id └────────────┘
src └────────────┘
typ └────────────┘
288
289 @[simp] theorem bUnion_of_singleton (s : set α) : (⋃ x ∈ s, {x}) = s :=
id └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └──┘ ┴ ┴
290 ext $ by simp
id └─┘
src └─┘ └────
typ └─┘ └────
doc └────
txt └────
par └────
pid └
st └─────
291
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
292 theorem bUnion_union (s t : set α) (u : α → set β) :
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
293 (⋃ x ∈ s ∪ t, u x) = (⋃ x ∈ s, u x) ∪ (⋃ x ∈ t, u x) :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
294 supr_union
id └────────┘
src └────────┘
typ └────────┘
295
296 -- TODO(Jeremy): once again, simp doesn't do it alone.
297
298 @[simp] theorem bUnion_insert (a : α) (s : set α) (t : α → set β) :
id ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └──┘
299 (⋃ x ∈ insert a s, t x) = t a ∪ (⋃ x ∈ s, t x) :=
id ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
300 begin rw [insert_eq], simp [bUnion_union] end
id └───────┘ └──────────┘
src └──┘└───────┘┴ └────┘└──────────┘└┘
typ └──┘└───────┘┴ └────┘└──────────┘└┘
doc └──┘ ┴ └────┘ └┘
txt └──┘ ┴ └────┘ └┘
par └──┘ ┴ └────┘ └┘
pid └┘ ┴ ┴┴ ┴┴
st └─────────────────┘└─────────────────────┘└─┘
301
302 theorem bUnion_pair (a b : α) (s : α → set β) :
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
303 (⋃ x ∈ ({a, b} : set α), s x) = s a ∪ s b :=
id ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
304 by rw insert_of_has_insert; simp [union_comm]
id └──────────────────┘ └────────┘
src └─┘└──────────────────┘ └────┘└────────┘└─
typ └─┘└──────────────────┘ └────┘└────────┘└─
doc └─┘ └────┘ └─
txt └─┘ └────┘ └─
par └─┘ └────┘ └─
pid ┴ ┴┴ ┴└
st └───────────────────────────────────────────
305
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
306 @[simp] -- complete_boolean_algebra
doc └──┘
307 theorem compl_bUnion (s : set α) (t : α → set β) : - (⋃ i ∈ s, t i) = (⋂ i ∈ s, - t i) :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
308 ext (λ x, by simp)
id └─┘ ┴
src └─┘ └──┘
typ └─┘ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
309
310 -- classical -- complete_boolean_algebra
311 theorem compl_bInter (s : set α) (t : α → set β) : -(⋂ i ∈ s, t i) = (⋃ i ∈ s, - t i) :=
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
312 ext (λ x, by simp [classical.not_forall])
id └─┘ ┴ └──────────────────┘
src └─┘ └────┘└──────────────────┘┴
typ └─┘ ┴ └────┘└──────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └──────────────────────────┘
313
314 theorem inter_bUnion (s : set α) (t : α → set β) (u : set β) :
id └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴
315 u ∩ (⋃ i ∈ s, t i) = ⋃ i ∈ s, u ∩ t i :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
316 begin
st └─────
317 ext x,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
318 simp only [exists_prop, mem_Union, mem_inter_eq],
id └─────────┘ └───────┘ └──────────┘
src └─────────┘└─────────┘└┘└───────┘└┘└──────────┘┴
typ └─────────┘└─────────┘└┘└───────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────┘└─
319 exact ⟨λ ⟨hx, ⟨i, is, xi⟩⟩, ⟨i, is, hx, xi⟩, λ ⟨i, is, hx, xi⟩, ⟨hx, ⟨i, is, xi⟩⟩⟩
id └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘
src └────┘ └┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └──┘
typ └────┘ └┘└┘└┘ ┴└┘└┘└┘└┘└──┘ └┘ └┘ └┘ └─┘ └┘┴└┘└┘└┘└┘└┘└┘└─┘ └┘ └┘ └┘ └──┘
doc └────┘ └┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └──┘
txt └────┘ └┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └──┘
par └────┘ └┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └──┘
pid ┴ └┘ └┘ └┘ └┘ └──┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘ └─┘┴
st ────────────────────────────────────────────────────────────────────────────────────┘
320 end
st └─┘
321
322 theorem bUnion_inter (s : set α) (t : α → set β) (u : set β) :
id └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴
323 (⋃ i ∈ s, t i) ∩ u = (⋃ i ∈ s, t i ∩ u) :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
324 by simp [@inter_comm _ _ u, inter_bUnion]
id └────────┘ ┴ └──────────┘
src └────┘ └────────┘└───┘ └┘└──────────┘└─
typ └────┘ └────────┘└───┘┴└┘└──────────┘└─
doc └────┘ └───┘ └┘ └─
txt └────┘ └───┘ └┘ └─
par └────┘ └───┘ └┘ └─
pid ┴┴ └───┘ └┘ ┴└
st └───────────────────────────────────────
325
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
326 /-- Intersection of a set of sets. -/
327 @[reducible] def sInter (S : set (set α)) : set α := Inf S
id └─┘ └─┘ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘ └─┘ └─┘
typ └─┘ └─┘ ┴ └─┘ ┴ └─┘ ┴
doc └───────┘ └─┘
328
329 prefix `⋂₀`:110 := sInter
id └────┘
src └────┘
typ └────┘
doc └────┘
330
331 theorem mem_sUnion_of_mem {x : α} {t : set α} {S : set (set α)} (hx : x ∈ t) (ht : t ∈ S) :
id ┴ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └─┘ ┴ ┴
typ ┴ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
332 x ∈ ⋃₀ S :=
id ┴ ┴ └┘ ┴
src ┴ └┘
typ ┴ ┴ └┘ ┴
333 ⟨t, ⟨ht, hx⟩⟩
id ┴ └┘ └┘
typ ┴ └┘ └┘
334
335 @[simp] theorem mem_sUnion {x : α} {S : set (set α)} : x ∈ ⋃₀ S ↔ ∃t ∈ S, x ∈ t := iff.rfl
id ┴ └─┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └─────┘
src └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └─────┘
typ ┴ └─┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └─────┘
doc └──┘
336
337 -- is this theorem really necessary?
338 theorem not_mem_of_not_mem_sUnion {x : α} {t : set α} {S : set (set α)}
id ┴ └─┘ ┴ └─┘ └─┘ ┴
src └─┘ └─┘ └─┘
typ ┴ └─┘ ┴ └─┘ └─┘ ┴
339 (hx : x ∉ ⋃₀ S) (ht : t ∈ S) : x ∉ t :=
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
340 λ h, hx ⟨t, ht, h⟩
id ┴ └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴
341
342 @[simp] theorem mem_sInter {x : α} {S : set (set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t := iff.rfl
id ┴ └─┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─┘ └─┘ ┴ └┘ ┴ ┴ └─────┘
typ ┴ └─┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ └┘
343
344 theorem sInter_subset_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : ⋂₀ S ⊆ t :=
id └─┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ └─┘ └─┘ ┴ └┘ ┴
typ └─┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘
345 Inf_le tS
id └────┘ └┘
src └────┘
typ └────┘ └┘
346
347 theorem subset_sUnion_of_mem {S : set (set α)} {t : set α} (tS : t ∈ S) : t ⊆ ⋃₀ S :=
id └─┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └─┘ └─┘ └─┘ ┴ ┴ └┘
typ └─┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
348 le_Sup tS
id └────┘ └┘
src └────┘
typ └────┘ └┘
349
350 lemma subset_sUnion_of_subset {s : set α} (t : set (set α)) (u : set α) (h₁ : s ⊆ u)
id └─┘ ┴ └─┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ └─┘ └─┘ ┴
typ └─┘ ┴ └─┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴
351 (h₂ : u ∈ t) : s ⊆ ⋃₀ t :=
id ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴
352 subset.trans h₁ (subset_sUnion_of_mem h₂)
id └──────────┘ └┘ └──────────────────┘ └┘
src └──────────┘ └──────────────────┘
typ └──────────┘ └┘ └──────────────────┘ └┘
353
354 theorem sUnion_subset {S : set (set α)} {t : set α} (h : ∀t' ∈ S, t' ⊆ t) : (⋃₀ S) ⊆ t :=
id └─┘ └─┘ ┴ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ └─┘ └─┘ ┴ └┘ ┴
typ └─┘ └─┘ ┴ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
355 Sup_le h
id └────┘ ┴
src └────┘
typ └────┘ ┴
356
357 theorem sUnion_subset_iff {s : set (set α)} {t : set α} : ⋃₀ s ⊆ t ↔ ∀t' ∈ s, t' ⊆ t :=
id └─┘ └─┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
src └─┘ └─┘ └─┘ └┘ ┴ ┴ ┴
typ └─┘ └─┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
358 ⟨assume h t' ht', subset.trans (subset_sUnion_of_mem ht') h, sUnion_subset⟩
id ┴ └┘ └─┘ └──────────┘ └──────────────────┘ └─┘ ┴ └───────────┘
src └──────────┘ └──────────────────┘ └───────────┘
typ ┴ └┘ └─┘ └──────────┘ └──────────────────┘ └─┘ ┴ └───────────┘
359
360 theorem subset_sInter {S : set (set α)} {t : set α} (h : ∀t' ∈ S, t ⊆ t') : t ⊆ (⋂₀ S) :=
id └─┘ └─┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ └─┘ └─┘ ┴ ┴ └┘
typ └─┘ └─┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘
361 le_Inf h
id └────┘ ┴
src └────┘
typ └────┘ ┴
362
363 theorem sUnion_subset_sUnion {S T : set (set α)} (h : S ⊆ T) : ⋃₀ S ⊆ ⋃₀ T :=
id └─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ └─┘ ┴ └┘ ┴ └┘
typ └─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
364 sUnion_subset $ λ s hs, subset_sUnion_of_mem (h hs)
id └───────────┘ ┴ └┘ └──────────────────┘ ┴ └┘
src └───────────┘ └──────────────────┘
typ └───────────┘ ┴ └┘ └──────────────────┘ ┴ └┘
365
366 theorem sInter_subset_sInter {S T : set (set α)} (h : S ⊆ T) : ⋂₀ T ⊆ ⋂₀ S :=
id └─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ └─┘ ┴ └┘ ┴ └┘
typ └─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘
367 subset_sInter $ λ s hs, sInter_subset_of_mem (h hs)
id └───────────┘ ┴ └┘ └──────────────────┘ ┴ └┘
src └───────────┘ └──────────────────┘
typ └───────────┘ ┴ └┘ └──────────────────┘ ┴ └┘
368
369 @[simp] theorem sUnion_empty : ⋃₀ ∅ = (∅ : set α) := Sup_empty
id └┘ ┴ ┴ ┴ └─┘ ┴ └───────┘
src └┘ ┴ ┴ ┴ └─┘ └───────┘
typ └┘ ┴ ┴ ┴ └─┘ ┴ └───────┘
doc └──┘
370
371 @[simp] theorem sInter_empty : ⋂₀ ∅ = (univ : set α) := Inf_empty
id └┘ ┴ ┴ └──┘ └─┘ ┴ └───────┘
src └┘ ┴ ┴ └──┘ └─┘ └───────┘
typ └┘ ┴ ┴ └──┘ └─┘ ┴ └───────┘
doc └──┘ └┘
372
373 @[simp] theorem sUnion_singleton (s : set α) : ⋃₀ {s} = s := Sup_singleton
id └─┘ ┴ └┘ ┴┴ ┴ ┴ └───────────┘
src └─┘ └┘ ┴ ┴ └───────────┘
typ └─┘ ┴ └┘ ┴┴ ┴ ┴ └───────────┘
doc └──┘
374
375 @[simp] theorem sInter_singleton (s : set α) : ⋂₀ {s} = s := Inf_singleton
id └─┘ ┴ └┘ ┴┴ ┴ ┴ └───────────┘
src └─┘ └┘ ┴ ┴ └───────────┘
typ └─┘ ┴ └┘ ┴┴ ┴ ┴ └───────────┘
doc └──┘ └┘
376
377 theorem sUnion_union (S T : set (set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T := Sup_union
id └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └───────┘
src └─┘ └─┘ └┘ ┴ ┴ └┘ ┴ └┘ └───────┘
typ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └───────┘
378
379 theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T := Inf_union
id └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └───────┘
src └─┘ └─┘ └┘ ┴ ┴ └┘ ┴ └┘ └───────┘
typ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └───────┘
doc └┘ └┘ └┘
380
381 @[simp] theorem sUnion_insert (s : set α) (T : set (set α)) : ⋃₀ (insert s T) = s ∪ ⋃₀ T := Sup_insert
id └─┘ ┴ └─┘ └─┘ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────────┘
src └─┘ └─┘ └─┘ └┘ └────┘ ┴ ┴ └┘ └────────┘
typ └─┘ ┴ └─┘ └─┘ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────────┘
doc └──┘
382
383 @[simp] theorem sInter_insert (s : set α) (T : set (set α)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T := Inf_insert
id └─┘ ┴ └─┘ └─┘ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────────┘
src └─┘ └─┘ └─┘ └┘ └────┘ ┴ ┴ └┘ └────────┘
typ └─┘ ┴ └─┘ └─┘ ┴ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────────┘
doc └──┘ └┘ └┘
384
385 theorem sUnion_pair (s t : set α) : ⋃₀ {s, t} = s ∪ t :=
id └─┘ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
386 (sUnion_insert _ _).trans $ by rw [union_comm, sUnion_singleton]
id └───────────┘ └───┘ └────────┘ └──────────────┘
src └───────────┘ └───┘ └──┘└────────┘└┘└──────────────┘└─
typ └───────────┘ └───┘ └──┘└────────┘└┘└──────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────┘└────────────────┘┴└
387
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
388 theorem sInter_pair (s t : set α) : ⋂₀ {s, t} = s ∩ t :=
id └─┘ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └┘ ┴ ┴ ┴ ┴
typ └─┘ ┴ └┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
doc └┘
389 (sInter_insert _ _).trans $ by rw [inter_comm, sInter_singleton]
id └───────────┘ └───┘ └────────┘ └──────────────┘
src └───────────┘ └───┘ └──┘└────────┘└┘└──────────────┘└─
typ └───────────┘ └───┘ └──┘└────────┘└┘└──────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────┘└────────────────┘┴└
390
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
391 @[simp] theorem sUnion_image (f : α → set β) (s : set α) : ⋃₀ (f '' s) = ⋃ x ∈ s, f x := Sup_image
id ┴ └─┘ ┴ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───────┘
src └─┘ └─┘ └┘ └┘ ┴ ┴ ┴ └───────┘
typ ┴ └─┘ ┴ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───────┘
doc └──┘ ┴ ┴
392
393 @[simp] theorem sInter_image (f : α → set β) (s : set α) : ⋂₀ (f '' s) = ⋂ x ∈ s, f x := Inf_image
id ┴ └─┘ ┴ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───────┘
src └─┘ └─┘ └┘ └┘ ┴ ┴ ┴ └───────┘
typ ┴ └─┘ ┴ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └───────┘
doc └──┘ └┘ ┴ ┴
394
395 @[simp] theorem sUnion_range (f : ι → set β) : ⋃₀ (range f) = ⋃ x, f x := Sup_range
id ┴ └─┘ ┴ └┘ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └───────┘
src └─┘ └┘ └───┘ ┴ ┴ ┴ └───────┘
typ ┴ └─┘ ┴ └┘ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └───────┘
doc └──┘ └───┘ ┴ ┴
396
397 @[simp] theorem sInter_range (f : ι → set β) : ⋂₀ (range f) = ⋂ x, f x := Inf_range
id ┴ └─┘ ┴ └┘ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └───────┘
src └─┘ └┘ └───┘ ┴ ┴ ┴ └───────┘
typ ┴ └─┘ ┴ └┘ └───┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └───────┘
doc └──┘ └┘ └───┘ ┴ ┴
398
399 lemma sUnion_eq_univ_iff {c : set (set α)} :
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
400 ⋃₀ c = @set.univ α ↔ ∀ a, ∃ b ∈ c, a ∈ b :=
id └┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └┘ ┴ └──────┘ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
401 ⟨λ H a, let ⟨b, hm, hb⟩ := mem_sUnion.1 $ by rw H; exact mem_univ a in ⟨b, hm, hb⟩,
id ┴ ┴ └─┘ ┴ └┘ └┘ └────────┘┴ ┴ └──────┘ ┴
src └────────┘┴ └─┘ └────┘└──────┘┴ ┴
typ ┴ ┴ └─┘ ┴ └┘ └┘ └────────┘┴ └─┘┴ └────┘└──────┘┴┴┴
doc └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └──────────────────────┘
402 λ H, set.univ_subset_iff.1 $ λ x hx, let ⟨b, hm, hb⟩ := H x in set.mem_sUnion_of_mem hb hm⟩
id ┴ └─────────────────┘┴ ┴ └┘ └─┘ └┘ └┘ ┴ ┴ └───────────────────┘
src └─────────────────┘┴ └───────────────────┘
typ ┴ └─────────────────┘┴ ┴ └┘ └─┘ └┘ └┘ ┴ ┴ └───────────────────┘
403
404 theorem compl_sUnion (S : set (set α)) :
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
405 - ⋃₀ S = ⋂₀ (compl '' S) :=
id ┴ └┘ ┴ ┴ └┘ └───┘ └┘ ┴
src ┴ └┘ ┴ └┘ └───┘ └┘
typ ┴ └┘ ┴ ┴ └┘ └───┘ └┘ ┴
doc └┘
406 set.ext $ assume x,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
407 ⟨assume : ¬ (∃s∈S, x ∈ s), assume s h,
id ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
408 match s, h with
id ┴ ┴
typ ┴ ┴
409 ._, ⟨t, hs, rfl⟩ := assume h, this ⟨t, hs, h⟩
id ┴ └┘ └─┘ ┴ └──┘ ┴
src └─┘
typ ┴ └┘ └─┘ ┴ └──┘ ┴
410 end,
411 assume : ∀s, s ∈ compl '' S → x ∈ s,
id ┴ ┴ ┴ └───┘ └┘ ┴ ┴ ┴ ┴
src ┴ └───┘ └┘ ┴
typ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ ┴ ┴
412 assume ⟨t, tS, xt⟩, this (compl t) (mem_image_of_mem _ tS) xt⟩
id ┴┴ └┘ └┘ └──┘ └───┘ └──────────────┘
src └───┘ └──────────────┘
typ ┴┴ └┘ └┘ └──┘ └───┘ └──────────────┘
413
414 -- classical
415 theorem sUnion_eq_compl_sInter_compl (S : set (set α)) :
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
416 ⋃₀ S = - ⋂₀ (compl '' S) :=
id └┘ ┴ ┴ ┴ └┘ └───┘ └┘ ┴
src └┘ ┴ ┴ └┘ └───┘ └┘
typ └┘ ┴ ┴ ┴ └┘ └───┘ └┘ ┴
doc └┘
417 by rw [←compl_compl (⋃₀ S), compl_sUnion]
id └─────────┘ └┘ ┴ └──────────┘
src └───┘└─────────┘┴ └┘┴ └─┘└──────────┘└─
typ └───┘└─────────┘┴ └┘┴┴└─┘└──────────┘└─
doc └───┘ ┴ ┴ └─┘ └─
txt └───┘ ┴ ┴ └─┘ └─
par └───┘ ┴ ┴ └─┘ └─
pid └─┘ ┴ ┴ └─┘ ┴└
st └──────────────────────┘└────────────┘┴└
418
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
419 -- classical
src ────────────┘
typ ────────────┘
doc ────────────┘
txt ────────────┘
par ────────────┘
pid ────────────┘
st ────────────┘
420 theorem compl_sInter (S : set (set α)) :
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
421 - ⋂₀ S = ⋃₀ (compl '' S) :=
id ┴ └┘ ┴ ┴ └┘ └───┘ └┘ ┴
src ┴ └┘ ┴ └┘ └───┘ └┘
typ ┴ └┘ ┴ ┴ └┘ └───┘ └┘ ┴
doc └┘
422 by rw [sUnion_eq_compl_sInter_compl, compl_compl_image]
id └──────────────────────────┘ └───────────────┘
src └──┘└──────────────────────────┘└┘└───────────────┘└─
typ └──┘└──────────────────────────┘└┘└───────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────────────────────────┘└─────────────────┘┴└
423
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
424 -- classical
src ────────────┘
typ ────────────┘
doc ────────────┘
txt ────────────┘
par ────────────┘
pid ────────────┘
st ────────────┘
425 theorem sInter_eq_comp_sUnion_compl (S : set (set α)) :
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
426 ⋂₀ S = -(⋃₀ (compl '' S)) :=
id └┘ ┴ ┴ ┴ └┘ └───┘ └┘ ┴
src └┘ ┴ ┴ └┘ └───┘ └┘
typ └┘ ┴ ┴ ┴ └┘ └───┘ └┘ ┴
doc └┘
427 by rw [←compl_compl (⋂₀ S), compl_sInter]
id └─────────┘ └┘ ┴ └──────────┘
src └───┘└─────────┘┴ └┘┴ └─┘└──────────┘└─
typ └───┘└─────────┘┴ └┘┴┴└─┘└──────────┘└─
doc └───┘ ┴ └┘┴ └─┘ └─
txt └───┘ ┴ ┴ └─┘ └─
par └───┘ ┴ ┴ └─┘ └─
pid └─┘ ┴ ┴ └─┘ ┴└
st └──────────────────────┘└────────────┘┴└
428
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
429 theorem inter_empty_of_inter_sUnion_empty {s t : set α} {S : set (set α)} (hs : t ∈ S)
id └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ └─┘ ┴
typ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴
430 (h : s ∩ ⋃₀ S = ∅) :
id ┴ ┴ └┘ ┴ ┴ ┴
src ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴
431 s ∩ t = ∅ :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
432 eq_empty_of_subset_empty $ by rw ← h; exact
id └──────────────────────┘ ┴
src └──────────────────────┘ └───┘ └────┘
typ └──────────────────────┘ └───┘┴ └────┘
doc └───┘ └────┘
txt └───┘ └────┘
par └───┘ └────┘
pid └─┘ ┴
st └──────────────
433 inter_subset_inter_right _ (subset_sUnion_of_mem hs)
id └──────────────────────┘ └──────────────────┘ └┘
src └──────────────────────┘└─┘ └──────────────────┘┴ └─
typ └──────────────────────┘└─┘ └──────────────────┘┴└┘└─
doc └─┘ ┴ └─
txt └─┘ ┴ └─
par └─┘ ┴ └─
pid └─┘ ┴ ┴└
st ─────────────────────────────────────────────────────
434
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
435 theorem range_sigma_eq_Union_range {γ : α → Type*} (f : sigma γ → β) :
id ┴ └───┘ ┴ ┴
src └───┘
typ ┴ └───┘ ┴ ┴
436 range f = ⋃ a, range (λ b, f ⟨a, b⟩) :=
id └───┘ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ └───┘
typ └───┘ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘ ┴ ┴ └───┘
437 set.ext $ by simp
id └─────┘
src └─────┘ └────
typ └─────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
438
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
439 theorem Union_eq_range_sigma (s : α → set β) : (⋃ i, s i) = range (λ a : Σ i, s i, a.2) :=
id ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └───┘ ┴ ┴┴ ┴ ┴ ┴┴
src └─┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └───┘ ┴ ┴┴ ┴ ┴ ┴┴
doc ┴ ┴ └───┘
440 by simp [set.ext_iff]
id └─────────┘
src └────┘└─────────┘└─
typ └────┘└─────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────
441
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
442 theorem Union_image_preimage_sigma_mk_eq_self {ι : Type*} {σ : ι → Type*} (s : set (sigma σ)) :
id ┴ └─┘ └───┘ ┴
src └─┘ └───┘
typ ┴ └─┘ └───┘ ┴
443 (⋃ i, sigma.mk i '' (sigma.mk i ⁻¹' s)) = s :=
id ┴ ┴┴ └──────┘ ┴ └┘ └──────┘ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ └──────┘ └┘ └──────┘ └─┘ ┴
typ ┴ ┴┴ └──────┘ ┴ └┘ └──────┘ ┴ └─┘ ┴ ┴ ┴
doc ┴ ┴ └─┘
444 begin
st └─────
445 ext x,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
446 simp only [mem_Union, mem_image, mem_preimage],
id └───────┘ └───────┘ └──────────┘
src └─────────┘└───────┘└┘└───────┘└┘└──────────┘┴
typ └─────────┘└───────┘└┘└───────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ───────────────────────────────────────────────┘└─
447 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
448 { rintros ⟨i, a, h, rfl⟩, exact h },
id ┴
src └────────────────────┘ └────┘ ┴
typ └────────────────────┘ └────┘┴┴
doc └────────────────────┘ └────┘ ┴
txt └────────────────────┘ └────┘ ┴
par └────────────────────┘ └────┘ ┴
pid └─────────────┘ ┴ ┴
st ───┘└────────────────────┘└────────┘└┘└
449 { intro h, cases x with i a, exact ⟨i, a, h, rfl⟩ }
id ┴ ┴ ┴ ┴ └─┘
src └─────┘ └────┘ └───────┘ └────┘ └┘ └┘ └┘└─┘└┘
typ └─────┘ └────┘┴└───────┘ └────┘ ┴└┘┴└┘┴└┘└─┘└┘
doc └─────┘ └────┘ └───────┘ └────┘ └┘ └┘ └┘ └┘
txt └─────┘ └────┘ └───────┘ └────┘ └┘ └┘ └┘ └┘
par └─────┘ └────┘ └───────┘ └────┘ └┘ └┘ └┘ └┘
pid └┘ ┴ └───────┘ ┴ └┘ └┘ └┘ ┴┴
st ──────────┘└────────────────┘└─────────────────────┘└─
450 end
st ──┘
451
452 lemma sUnion_mono {s t : set (set α)} (h : s ⊆ t) : (⋃₀ s) ⊆ (⋃₀ t) :=
id └─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ └─┘ ┴ └┘ ┴ └┘
typ └─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
453 sUnion_subset $ assume t' ht', subset_sUnion_of_mem $ h ht'
id └───────────┘ └┘ └─┘ └──────────────────┘ ┴ └─┘
src └───────────┘ └──────────────────┘
typ └───────────┘ └┘ └─┘ └──────────────────┘ ┴ └─┘
454
455 lemma Union_subset_Union {s t : ι → set α} (h : ∀i, s i ⊆ t i) : (⋃i, s i) ⊆ (⋃i, t i) :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
456 @supr_le_supr (set α) ι _ s t h
id └──────────┘ └─┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ └─┘
typ └──────────┘ └─┘ ┴ ┴ ┴ ┴ ┴
457
458 lemma Union_subset_Union2 {ι₂ : Sort*} {s : ι → set α} {t : ι₂ → set α} (h : ∀i, ∃j, s i ⊆ t j) :
id ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴
459 (⋃i, s i) ⊆ (⋃i, t i) :=
id ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
460 @supr_le_supr2 (set α) ι ι₂ _ s t h
id └───────────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴
461
462 lemma Union_subset_Union_const {ι₂ : Sort x} {s : set α} (h : ι → ι₂) : (⋃ i:ι, s) ⊆ (⋃ j:ι₂, s) :=
id └─┘ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ └┘┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ └┘┴ ┴
doc ┴ ┴ ┴ ┴
463 @supr_le_supr_const (set α) ι ι₂ _ s h
id └────────────────┘ └─┘ ┴ ┴ └┘ ┴ ┴
src └────────────────┘ └─┘
typ └────────────────┘ └─┘ ┴ ┴ └┘ ┴ ┴
464
465 @[simp] lemma Union_of_singleton (α : Type u) : (⋃(x : α), {x}) = @set.univ α :=
id ┴ ┴ ┴ ┴┴ ┴ └──────┘ ┴
src ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴┴ ┴ └──────┘ ┴
doc └──┘ ┴ ┴
466 ext $ λ x, ⟨λ h, ⟨⟩, λ h, ⟨{x}, ⟨⟨x, rfl⟩, mem_singleton x⟩⟩⟩
id └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ └───────────┘ ┴
src └─┘ ┴ ┴ └─┘ └───────────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ └───────────┘ ┴
467
468 theorem bUnion_subset_Union (s : set α) (t : α → set β) :
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
469 (⋃ x ∈ s, t x) ⊆ (⋃ x, t x) :=
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
doc ┴ ┴ ┴ ┴
470 Union_subset_Union $ λ i, Union_subset $ λ h, by refl
id └────────────────┘ ┴ └──────────┘ ┴
src └────────────────┘ └──────────┘ └────
typ └────────────────┘ ┴ └──────────┘ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
471
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
472 lemma sUnion_eq_bUnion {s : set (set α)} : (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) :=
id └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └┘ ┴ ┴ └─┘ ┴ ┴
typ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
473 set.ext $ by simp
id └─────┘
src └─────┘ └────
typ └─────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
474
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
475 lemma sInter_eq_bInter {s : set (set α)} : (⋂₀ s) = (⋂ (i : set α) (h : i ∈ s), i) :=
id └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └┘ ┴ ┴ └─┘ ┴ ┴
typ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ ┴ ┴
476 set.ext $ by simp
id └─────┘
src └─────┘ └────
typ └─────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
477
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
478 lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i.1) :=
id └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴
src └─┘ └─┘ └┘ ┴ ┴ ┴ ┴
typ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴
doc ┴ ┴
479 set.ext $ λ x, by simp
id └─────┘ ┴
src └─────┘ └────
typ └─────┘ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
480
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
481 lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i.1) :=
id └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴
src └─┘ └─┘ └┘ ┴ ┴ ┴ ┴
typ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └┘ ┴ ┴
482 set.ext $ λ x, by simp
id └─────┘ ┴
src └─────┘ └────
typ └─────┘ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
483
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
484 lemma union_eq_Union {s₁ s₂ : set α} : s₁ ∪ s₂ = ⋃ b : bool, cond b s₁ s₂ :=
id └─┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘┴ └──┘ ┴ └┘ └┘
src └─┘ ┴ ┴ ┴ └──┘┴ └──┘
typ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘┴ └──┘ ┴ └┘ └┘
doc ┴ ┴
485 set.ext $ λ x, by simp [bool.exists_bool, or_comm]
id └─────┘ ┴ └──────────────┘ └─────┘
src └─────┘ └────┘└──────────────┘└┘└─────┘└─
typ └─────┘ ┴ └────┘└──────────────┘└┘└─────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────────────────
486
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
487 lemma inter_eq_Inter {s₁ s₂ : set α} : s₁ ∩ s₂ = ⋂ b : bool, cond b s₁ s₂ :=
id └─┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘┴ └──┘ ┴ └┘ └┘
src └─┘ ┴ ┴ ┴ └──┘┴ └──┘
typ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘┴ └──┘ ┴ └┘ └┘
doc ┴ ┴
488 set.ext $ λ x, by simp [bool.forall_bool, and_comm]
id └─────┘ ┴ └──────────────┘ └──────┘
src └─────┘ └────┘└──────────────┘└┘└──────┘└─
typ └─────┘ ┴ └────┘└──────────────┘└┘└──────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────────────────────
489
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
490 instance : complete_boolean_algebra (set α) :=
id └──────────────────────┘ └─┘ ┴
src └──────────────────────┘ └─┘
typ └──────────────────────┘ └─┘ ┴
doc └──────────────────────┘
491 { neg := compl,
id └───┘
src └───┘
typ └───┘
492 sub := (\),
id ┴
src ┴
typ ┴
493 inf_neg_eq_bot := assume s, ext $ assume x, ⟨assume ⟨h, nh⟩, nh h, false.elim⟩,
id ┴ └─┘ ┴ ┴┴ └┘ └────────┘
src └─┘ └────────┘
typ ┴ └─┘ ┴ ┴┴ └┘ └────────┘
494 sup_neg_eq_top := assume s, ext $ assume x, ⟨assume h, trivial, assume _, classical.em $ x ∈ s⟩,
id ┴ └─┘ ┴ ┴ └─────┘ ┴ └──────────┘ ┴ ┴ ┴
src └─┘ └─────┘ └──────────┘ ┴
typ ┴ └─┘ ┴ ┴ └─────┘ ┴ └──────────┘ ┴ ┴ ┴
495 le_sup_inf := distrib_lattice.le_sup_inf,
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
496 sub_eq := assume x y, rfl,
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
497 infi_sup_le_sup_Inf := assume s t x, show x ∈ (⋂ b ∈ t, s ∪ b) → x ∈ s ∪ (⋂₀ t),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc ┴ ┴ └┘
498 by simp; exact assume h,
src └──┘ └────┘ └───
typ └──┘ └────┘ └───
doc └──┘ └────┘ └───
txt └──┘ └────┘ └───
par └──┘ └────┘ └───
pid ┴ └───
st └──────────────────────
499 or.imp_right
id └──────────┘
src ─────┘└──────────┘└
typ ─────┘└──────────┘└
doc ─────┘ └
txt ─────┘ └
par ─────┘ └
pid ─────┘ └
st ───────────────────
500 (assume hn : x ∉ s, assume i hi, or.resolve_left (h i hi) hn)
id ┴ └─────────────┘
src ───────┘ └────┘ ┴┴┴ └┘ └─────┘└─────────────┘┴ ┴ ┴ └┘ └─
typ ───────┘ └────┘ ┴┴┴ └┘ └─────┘└─────────────┘┴ ┴ ┴ └┘ └─
doc ───────┘ └────┘ ┴ ┴ └┘ └─────┘ ┴ ┴ ┴ └┘ └─
txt ───────┘ └────┘ ┴ ┴ └┘ └─────┘ ┴ ┴ ┴ └┘ └─
par ───────┘ └────┘ ┴ ┴ └┘ └─────┘ ┴ ┴ ┴ └┘ └─
pid ───────┘ └────┘ ┴ ┴ └┘ └─────┘ ┴ ┴ ┴ └┘ └─
st ──────────────────────────────────────────────────────────────────────
501 (classical.em $ x ∈ s),
id └──────────┘ ┴ ┴
src ───────┘ └──────────┘┴ ┴ ┴ ┴ ┴
typ ───────┘ └──────────┘┴ ┴┴┴ ┴┴┴
doc ───────┘ ┴ ┴ ┴ ┴ ┴
txt ───────┘ ┴ ┴ ┴ ┴ ┴
par ───────┘ ┴ ┴ ┴ ┴ ┴
pid ───────┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────┘
502 inf_Sup_le_supr_inf := assume s t x, show x ∈ s ∩ (⋃₀ t) → x ∈ (⋃ b ∈ t, s ∩ b),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴
503 by simp [-and_imp, and.left_comm],
id └───────────┘
src └──────────────┘└───────────┘┴
typ └──────────────┘└───────────┘┴
doc └──────────────┘ ┴
txt └──────────────┘ ┴
par └──────────────┘ ┴
pid ┴└─────────┘ ┴
st └─────────────────────────────┘
504 ..set.lattice_set }
id └─────────────┘
src └─────────────┘
typ └─────────────┘
505
506 lemma sInter_union_sInter {S T : set (set α)} :
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
507 (⋂₀S) ∪ (⋂₀T) = (⋂p ∈ set.prod S T, (p : (set α) × (set α)).1 ∪ p.2) :=
id └┘┴ ┴ └┘┴ ┴ ┴┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴
src └┘ ┴ └┘ ┴ ┴ └──────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
typ └┘┴ ┴ └┘┴ ┴ ┴┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴
doc └┘ └┘ ┴ └──────┘ ┴
508 Inf_sup_Inf
id └─────────┘
src └─────────┘
typ └─────────┘
509
510 lemma sUnion_inter_sUnion {s t : set (set α)} :
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
511 (⋃₀s) ∩ (⋃₀t) = (⋃p ∈ set.prod s t, (p : (set α) × (set α )).1 ∩ p.2) :=
id └┘┴ ┴ └┘┴ ┴ ┴┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴
src └┘ ┴ └┘ ┴ ┴ └──────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
typ └┘┴ ┴ └┘┴ ┴ ┴┴ └──────┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴
doc ┴ └──────┘ ┴
512 Sup_inf_Sup
id └─────────┘
src └─────────┘
typ └─────────┘
513
514 lemma sInter_bUnion {S : set (set α)} {T : set α → set (set α)} (hT : ∀s∈S, s = ⋂₀ T s) :
id └─┘ └─┘ ┴ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └─┘ └─┘ └─┘ └─┘ └─┘ ┴ └┘
typ └─┘ └─┘ ┴ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
doc └┘
515 ⋂₀ (⋃s∈S, T s) = ⋂₀ S :=
id └┘ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ ┴ ┴ └┘
typ └┘ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
doc └┘ ┴ ┴ └┘
516 begin
st └─────
517 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
518 simp only [and_imp, exists_prop, set.mem_sInter, set.mem_Union, exists_imp_distrib],
id └─────┘ └─────────┘ └────────────┘ └───────────┘ └────────────────┘
src └─────────┘└─────┘└┘└─────────┘└┘└────────────┘└┘└───────────┘└┘└────────────────┘┴
typ └─────────┘└─────┘└┘└─────────┘└┘└────────────┘└┘└───────────┘└┘└────────────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────┘└─
519 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
520 { assume H s sS,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ───┘└───────────┘└─
521 rw [hT s sS, mem_sInter],
id └┘ ┴ └┘ └────────┘
src └──┘ ┴ ┴ └┘└────────┘┴
typ └──┘└┘┴┴┴└┘└┘└────────┘┴
doc └──┘ ┴ ┴ └┘ ┴
txt └──┘ ┴ ┴ └┘ ┴
par └──┘ ┴ ┴ └┘ ┴
pid └┘ ┴ ┴ └┘ ┴
st ──────────────┘└──────────┘└──
522 assume t tTs,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ───────────────┘└─
523 apply H t s sS tTs },
id ┴ ┴ ┴ └┘ └─┘
src └────┘ ┴ ┴ ┴ ┴ ┴
typ └────┘┴┴┴┴┴┴└┘┴└─┘┴
doc └────┘ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────┘└┘└
524 { assume H t s sS tTs,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └─────────────────┘
st ──────────────────────┘└─
525 have xs : x ∈ s := H s sS,
id ┴ ┴ ┴ ┴ ┴ └┘
src └────────┘ ┴┴┴ └──┘ ┴ ┴
typ └────────┘┴┴┴┴┴└──┘┴┴┴┴└┘
doc └────────┘ ┴ ┴ └──┘ ┴ ┴
txt └────────┘ ┴ ┴ └──┘ ┴ ┴
par └────────┘ ┴ ┴ └──┘ ┴ ┴
pid └─────┘└─┘ ┴ ┴ └──┘ ┴ ┴
st ────────────────────────────┘└─
526 have : s ⊆ t,
id ┴ ┴ ┴
src └─────┘ ┴┴┴
typ └─────┘┴┴┴┴┴
doc └─────┘ ┴ ┴
txt └─────┘ ┴ ┴
par └─────┘ ┴ ┴
pid └───┘└┘ ┴ ┴
st ───────────────┘└─
527 { have Z := hT s sS,
id └┘ ┴ └┘
src └────────┘ ┴ ┴
typ └────────┘└┘┴┴┴└┘
doc └────────┘ ┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ─────┘└───────────────┘└─
528 rw sInter_eq_bInter at Z,
id └──────────────┘
src └─┘└──────────────┘└───┘
typ └─┘└──────────────┘└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ─────────────────────────────┘└─
529 rw Z, apply bInter_subset_of_mem,
id ┴ └──────────────────┘
src └─┘ └────┘└──────────────────┘
typ └─┘┴ └────┘└──────────────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st ─────────┘└──────────────────────────┘└─
530 exact tTs },
id └─┘
src └────┘ ┴
typ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────┘└┘└
531 exact this xs }
id └──┘ └┘
src └────┘ ┴ ┴
typ └────┘└──┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────┘└─
532 end
st ──┘
533
534 lemma sUnion_bUnion {S : set (set α)} {T : set α → set (set α)} (hT : ∀s∈S, s = ⋃₀ T s) :
id └─┘ └─┘ ┴ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └─┘ └─┘ └─┘ └─┘ └─┘ ┴ └┘
typ └─┘ └─┘ ┴ └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
535 ⋃₀ (⋃s∈S, T s) = ⋃₀ S :=
id └┘ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ ┴ ┴ └┘
typ └┘ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
doc ┴ ┴
536 begin
st └─────
537 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
538 simp only [exists_prop, set.mem_Union, set.mem_set_of_eq],
id └─────────┘ └───────────┘ └───────────────┘
src └─────────┘└─────────┘└┘└───────────┘└┘└───────────────┘┴
typ └─────────┘└─────────┘└┘└───────────┘└┘└───────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────┘└─
539 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
540 { rintros ⟨t, ⟨⟨s, ⟨sS, tTs⟩⟩, xt⟩⟩,
src └───────────────────────────────┘
typ └───────────────────────────────┘
doc └───────────────────────────────┘
txt └───────────────────────────────┘
par └───────────────────────────────┘
pid └────────────────────────┘
st ───┘└───────────────────────────────┘└─
541 refine ⟨s, ⟨sS, _⟩⟩,
id ┴ └┘
src └─────┘ └┘ └───┘
typ └─────┘ ┴└┘ └┘└───┘
doc └─────┘ └┘ └───┘
txt └─────┘ └┘ └───┘
par └─────┘ └┘ └───┘
pid ┴ └┘ └───┘
st ──────────────────────┘└─
542 rw hT s sS,
id └┘ ┴ └┘
src └─┘ ┴ ┴
typ └─┘└┘┴┴┴└┘
doc └─┘ ┴ ┴
txt └─┘ ┴ ┴
par └─┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────┘└─
543 exact subset_sUnion_of_mem tTs xt },
id └──────────────────┘ └─┘ └┘
src └────┘└──────────────────┘┴ ┴ ┴
typ └────┘└──────────────────┘┴└─┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└┘└
544 { rintros ⟨s, ⟨sS, xs⟩⟩,
src └───────────────────┘
typ └───────────────────┘
doc └───────────────────┘
txt └───────────────────┘
par └───────────────────┘
pid └────────────┘
st ────────────────────────┘└─
545 rw hT s sS at xs,
id └┘ ┴ └┘
src └─┘ ┴ ┴ └────┘
typ └─┘└┘┴┴┴└┘└────┘
doc └─┘ ┴ ┴ └────┘
txt └─┘ ┴ ┴ └────┘
par └─┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ └────┘
st ───────────────────┘└─
546 rcases mem_sUnion.1 xs with ⟨t, tTs, xt⟩,
id └────────┘ └┘
src └─────┘└────────┘└─┘ └────────────────┘
typ └─────┘└────────┘└─┘└┘└────────────────┘
doc └─────┘ └─┘ └────────────────┘
txt └─────┘ └─┘ └────────────────┘
par └─────┘ └─┘ └────────────────┘
pid ┴ └─┘ └────────────────┘
st ───────────────────────────────────────────┘└─
547 exact ⟨t, ⟨⟨s, ⟨sS, tTs⟩⟩, xt⟩⟩ }
id ┴ ┴ └┘ └─┘ └┘
src └────┘ └┘ └┘ └┘ └──┘ └─┘
typ └────┘ ┴└┘ ┴└┘ └┘└┘└─┘└──┘└┘└─┘
doc └────┘ └┘ └┘ └┘ └──┘ └─┘
txt └────┘ └┘ └┘ └┘ └──┘ └─┘
par └────┘ └┘ └┘ └┘ └──┘ └─┘
pid ┴ └┘ └┘ └┘ └──┘ └┘┴
st ───────────────────────────────────┘└─
548 end
st ──┘
549
550 lemma Union_range_eq_sUnion {α β : Type*} (C : set (set α))
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
551 {f : ∀(s : C), β → s} (hf : ∀(s : C), surjective (f s)) :
id ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
552 (⋃(y : β), range (λ(s : C), (f s y).val)) = ⋃₀ C :=
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ ┴
src ┴ ┴ └───┘ └─┘ ┴ └┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ ┴
doc ┴ ┴ └───┘
553 begin
st └─────
554 ext x, split,
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └┘
st ──────┘└─────┘└─
555 { rintro ⟨s, ⟨y, rfl⟩, ⟨⟨s, hs⟩, rfl⟩⟩, refine ⟨_, hs, _⟩, exact (f ⟨s, hs⟩ y).2 },
id └┘ ┴ ┴ └┘ ┴
src └──────────────────────────────────┘ └─────┘ └─┘ └──┘ └────┘ ┴ └┘ └┘ └──┘
typ └──────────────────────────────────┘ └─────┘ └─┘└┘└──┘ └────┘ ┴┴ ┴└┘└┘└┘┴└──┘
doc └──────────────────────────────────┘ └─────┘ └─┘ └──┘ └────┘ ┴ └┘ └┘ └──┘
txt └──────────────────────────────────┘ └─────┘ └─┘ └──┘ └────┘ ┴ └┘ └┘ └──┘
par └──────────────────────────────────┘ └─────┘ └─┘ └──┘ └────┘ ┴ └┘ └┘ └──┘
pid └────────────────────────────┘ ┴ └─┘ └──┘ ┴ ┴ └┘ └┘ ┴└─┘
st ───┘└──────────────────────────────────┘└─────────────────┘└──────────────────────┘└┘└
556 { rintro ⟨s, hs, hx⟩, cases hf ⟨s, hs⟩ ⟨x, hx⟩ with y hy, refine ⟨_, ⟨y, rfl⟩, ⟨⟨s, hs⟩, _⟩⟩,
id └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ └┘
src └────────────────┘ └────┘ ┴ └┘ └┘ └┘ └─────────┘ └─────┘ └─┘ └┘└─┘└─┘ └┘ └────┘
typ └────────────────┘ └────┘└┘┴ ┴└┘└┘└┘ ┴└┘└┘└─────────┘ └─────┘ └─┘ ┴└┘└─┘└─┘ ┴└┘└┘└────┘
doc └────────────────┘ └────┘ ┴ └┘ └┘ └┘ └─────────┘ └─────┘ └─┘ └┘ └─┘ └┘ └────┘
txt └────────────────┘ └────┘ ┴ └┘ └┘ └┘ └─────────┘ └─────┘ └─┘ └┘ └─┘ └┘ └────┘
par └────────────────┘ └────┘ ┴ └┘ └┘ └┘ └─────────┘ └─────┘ └─┘ └┘ └─┘ └┘ └────┘
pid └──────────┘ ┴ ┴ └┘ └┘ └┘ ┴└────────┘ ┴ └─┘ └┘ └─┘ └┘ └────┘
st ─────────────────────┘└──────────────────────────────────┘└──────────────────────────────────┘└─
557 exact congr_arg subtype.val hy }
id └───────┘ └─────────┘ └┘
src └────┘└───────┘┴└─────────┘┴ ┴
typ └────┘└───────┘┴└─────────┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
558 end
st ──┘
559
560 lemma Union_range_eq_Union {ι α β : Type*} (C : ι → set α)
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
561 {f : ∀(x : ι), β → C x} (hf : ∀(x : ι), surjective (f x)) :
id ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
562 (⋃(y : β), range (λ(x : ι), (f x y).val)) = ⋃x, C x :=
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ └───┘ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴ └───┘ ┴ ┴
563 begin
st └─────
564 ext x, rw [mem_Union, mem_Union], split,
id └───────┘ └───────┘
src └───┘ └──┘└───────┘└┘└───────┘┴ └───┘
typ └───┘ └──┘└───────┘└┘└───────┘┴ └───┘
doc └───┘ └──┘ └┘ ┴ └───┘
txt └───┘ └──┘ └┘ ┴ └───┘
par └───┘ └──┘ └┘ ┴ └───┘
pid └┘ └┘ └┘ ┴
st ──────┘└─────────────┘└─────────┘└──────┘└─
565 { rintro ⟨y, ⟨i, rfl⟩⟩, exact ⟨i, (f i y).2⟩ },
id ┴ ┴ ┴
src └──────────────────┘ └────┘ └┘ ┴ ┴ └───┘
typ └──────────────────┘ └────┘ └┘ ┴┴┴┴┴└───┘
doc └──────────────────┘ └────┘ └┘ ┴ ┴ └───┘
txt └──────────────────┘ └────┘ └┘ ┴ ┴ └───┘
par └──────────────────┘ └────┘ └┘ ┴ ┴ └───┘
pid └────────────┘ ┴ └┘ ┴ ┴ └──┘┴
st ───┘└──────────────────┘└─────────────────────┘└┘└
566 { rintro ⟨i, hx⟩, cases hf i ⟨x, hx⟩ with y hy, refine ⟨y, ⟨i, congr_arg subtype.val hy⟩⟩ }
id └┘ ┴ ┴ └┘ ┴ ┴ └───────┘ └─────────┘ └┘
src └────────────┘ └────┘ ┴ ┴ └┘ └─────────┘ └─────┘ └┘ └┘└───────┘┴└─────────┘┴ └─┘
typ └────────────┘ └────┘└┘┴┴┴ ┴└┘└┘└─────────┘ └─────┘ ┴└┘ ┴└┘└───────┘┴└─────────┘┴└┘└─┘
doc └────────────┘ └────┘ ┴ ┴ └┘ └─────────┘ └─────┘ └┘ └┘ ┴ ┴ └─┘
txt └────────────┘ └────┘ ┴ ┴ └┘ └─────────┘ └─────┘ └┘ └┘ ┴ ┴ └─┘
par └────────────┘ └────┘ ┴ ┴ └┘ └─────────┘ └─────┘ └┘ └┘ ┴ ┴ └─┘
pid └──────┘ ┴ ┴ ┴ └┘ ┴└────────┘ ┴ └┘ └┘ ┴ ┴ └┘┴
st ─────────────────┘└────────────────────────────┘└──────────────────────────────────────────┘└─
567 end
st ──┘
568
569 @[simp] theorem sub_eq_diff (s t : set α) : s - t = s \ t := rfl
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └─┘ ┴ ┴ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
570
571 section
572
573 variables {p : Prop} {μ : p → set α}
id └─┘
src └─┘
typ └─┘
574
575 @[simp] lemma Inter_pos (hp : p) : (⋂h:p, μ h) = μ hp := infi_pos hp
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘ └──────┘ └┘
src ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘ └──────┘ └┘
doc └──┘ ┴ ┴
576
577 @[simp] lemma Inter_neg (hp : ¬ p) : (⋂h:p, μ h) = univ := infi_neg hp
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └──┘ └──────┘ └┘
src ┴ ┴ ┴ ┴ └──┘ └──────┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └──┘ └──────┘ └┘
doc └──┘ ┴ ┴
578
579 @[simp] lemma Union_pos (hp : p) : (⋃h:p, μ h) = μ hp := supr_pos hp
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘ └──────┘ └┘
src ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └┘ └──────┘ └┘
doc └──┘ ┴ ┴
580
581 @[simp] lemma Union_neg (hp : ¬ p) : (⋃h:p, μ h) = ∅ := supr_neg hp
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └──────┘ └┘
src ┴ ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └──────┘ └┘
doc └──┘ ┴ ┴
582
583 @[simp] lemma Union_empty {ι : Sort*} : (⋃i:ι, ∅:set α) = ∅ := supr_bot
id ┴ ┴┴ ┴ └─┘ ┴ ┴ ┴ └──────┘
src ┴ ┴ ┴ └─┘ ┴ ┴ └──────┘
typ ┴ ┴┴ ┴ └─┘ ┴ ┴ ┴ └──────┘
doc └──┘ ┴ ┴
584
585 @[simp] lemma Inter_univ {ι : Sort*} : (⋂i:ι, univ:set α) = univ := infi_top
id ┴ ┴┴ └──┘ └─┘ ┴ ┴ └──┘ └──────┘
src ┴ ┴ └──┘ └─┘ ┴ └──┘ └──────┘
typ ┴ ┴┴ └──┘ └─┘ ┴ ┴ └──┘ └──────┘
doc └──┘ ┴ ┴
586
587 end
588
589 section image
590
591 lemma image_Union {f : α → β} {s : ι → set α} : f '' (⋃ i, s i) = (⋃i, f '' s i) :=
id ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ └┘ ┴ ┴
src └─┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ └┘ ┴ ┴
doc ┴ ┴ ┴ ┴
592 begin
st └─────
593 apply set.ext, intro x,
id └─────┘
src └────┘└─────┘ └─────┘
typ └────┘└─────┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └┘
st ──────────────┘└───────┘└─
594 simp [image, exists_and_distrib_right.symm, -exists_and_distrib_right],
id └───┘
src └────┘└───┘└┘ └──────────────────────────┘
typ └────┘└───┘└┘└───────────────────────────┘└──────────────────────────┘
doc └────┘ └┘ └──────────────────────────┘
txt └────┘ └┘ └──────────────────────────┘
par └────┘ └┘ └──────────────────────────┘
pid ┴┴ └┘ └──────────────────────────┘
st ───────────────────────────────────────────────────────────────────────┘└─
595 exact exists_swap
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────┘
596 end
st └─┘
597
598 lemma univ_subtype {p : α → Prop} : (univ : set (subtype p)) = (⋃x (h : p x), {⟨x, h⟩}) :=
id ┴ └──┘ └─┘ └─────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └─┘ └─────┘ ┴ ┴ ┴ ┴
typ ┴ └──┘ └─┘ └─────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
599 set.ext $ assume ⟨x, h⟩, by simp [h]
id └─────┘ ┴ ┴
src └─────┘ └────┘ └─
typ └─────┘ ┴ └────┘┴└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────
600
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
601 lemma range_eq_Union {ι} (f : ι → α) : range f = (⋃i, {f i}) :=
id ┴ ┴ └───┘ ┴ ┴ ┴┴┴ ┴┴ ┴
src └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴┴┴ ┴┴ ┴
doc └───┘ ┴ ┴
602 set.ext $ assume a, by simp [@eq_comm α a]
id └─────┘ ┴ └─────┘ ┴ ┴
src └─────┘ └────┘ └─────┘┴ ┴ └─
typ └─────┘ ┴ └────┘ └─────┘┴┴┴┴└─
doc └────┘ ┴ ┴ └─
txt └────┘ ┴ ┴ └─
par └────┘ ┴ ┴ └─
pid ┴┴ ┴ ┴ ┴└
st └────────────────────
603
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
604 lemma image_eq_Union (f : α → β) (s : set α) : f '' s = (⋃i∈s, {f i}) :=
id ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴┴ ┴┴ ┴
src └─┘ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴┴ ┴┴ ┴┴ ┴
doc ┴ ┴
605 set.ext $ assume b, by simp [@eq_comm β b]
id └─────┘ ┴ └─────┘ ┴ ┴
src └─────┘ └────┘ └─────┘┴ ┴ └─
typ └─────┘ ┴ └────┘ └─────┘┴┴┴┴└─
doc └────┘ ┴ ┴ └─
txt └────┘ ┴ ┴ └─
par └────┘ ┴ ┴ └─
pid ┴┴ ┴ ┴ ┴└
st └────────────────────
606
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
607 lemma bUnion_range {f : ι → α} {g : α → set β} : (⋃x ∈ range f, g x) = (⋃y, g (f y)) :=
id ┴ ┴ ┴ └─┘ ┴ ┴┴ └───┘ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src └─┘ ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴┴ └───┘ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ └───┘ ┴ ┴ ┴
608 by rw [← sUnion_image, ← range_comp, sUnion_range]
id └──────────┘ └────────┘ └──────────┘
src └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
typ └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
doc └────┘ └──┘ └┘ └─
txt └────┘ └──┘ └┘ └─
par └────┘ └──┘ └┘ └─
pid └──┘ └──┘ └┘ ┴└
st └─────────────────┘└────────────┘└────────────┘┴└
609
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
610 lemma bInter_range {f : ι → α} {g : α → set β} : (⋂x ∈ range f, g x) = (⋂y, g (f y)) :=
id ┴ ┴ ┴ └─┘ ┴ ┴┴ └───┘ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
src └─┘ ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴┴ └───┘ ┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴
doc ┴ └───┘ ┴ ┴ ┴
611 by rw [← sInter_image, ← range_comp, sInter_range]
id └──────────┘ └────────┘ └──────────┘
src └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
typ └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
doc └────┘ └──┘ └┘ └─
txt └────┘ └──┘ └┘ └─
par └────┘ └──┘ └┘ └─
pid └──┘ └──┘ └┘ ┴└
st └─────────────────┘└────────────┘└────────────┘┴└
612
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
613 variables {s : set γ} {f : γ → α} {g : α → set β}
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
614
615 lemma bUnion_image : (⋃x∈ (f '' s), g x) = (⋃y ∈ s, g (f y)) :=
id ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴ ┴
typ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
616 by rw [← sUnion_image, ← image_comp, sUnion_image]
id └──────────┘ └────────┘ └──────────┘
src └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
typ └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
doc └────┘ └──┘ └┘ └─
txt └────┘ └──┘ └┘ └─
par └────┘ └──┘ └┘ └─
pid └──┘ └──┘ └┘ ┴└
st └─────────────────┘└────────────┘└────────────┘┴└
617
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
618 lemma bInter_image : (⋂x∈ (f '' s), g x) = (⋂y ∈ s, g (f y)) :=
id ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴ ┴
typ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴
619 by rw [← sInter_image, ← image_comp, sInter_image]
id └──────────┘ └────────┘ └──────────┘
src └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
typ └────┘└──────────┘└──┘└────────┘└┘└──────────┘└─
doc └────┘ └──┘ └┘ └─
txt └────┘ └──┘ └┘ └─
par └────┘ └──┘ └┘ └─
pid └──┘ └──┘ └┘ ┴└
st └─────────────────┘└────────────┘└────────────┘┴└
620
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
621 end image
622
623 section preimage
624
625 theorem monotone_preimage {f : α → β} : monotone (preimage f) := assume a b h, preimage_mono h
id ┴ ┴ └──────┘ └──────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴
src └──────┘ └──────┘ └───────────┘
typ ┴ ┴ └──────┘ └──────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴
doc └──────┘ └──────┘
626
627 @[simp] theorem preimage_Union {ι : Sort w} {f : α → β} {s : ι → set β} :
id ┴ ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ ┴ └─┘ ┴
doc └──┘
628 preimage f (⋃i, s i) = (⋃i, preimage f (s i)) :=
id └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
typ └──────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ └──────┘ ┴ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴ └──────┘
629 set.ext $ by simp [preimage]
id └─────┘ └──────┘
src └─────┘ └────┘└──────┘└─
typ └─────┘ └────┘└──────┘└─
doc └────┘└──────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────
630
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
631 theorem preimage_bUnion {ι} {f : α → β} {s : set ι} {t : ι → set β} :
id ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
632 preimage f (⋃i ∈ s, t i) = (⋃i ∈ s, preimage f (t i)) :=
id └──────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ └──────┘ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
typ └──────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ └──────┘ ┴ ┴ ┴
doc └──────┘ ┴ ┴ ┴ ┴ └──────┘
633 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
634
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
635 @[simp] theorem preimage_sUnion {f : α → β} {s : set (set β)} :
id ┴ ┴ └─┘ └─┘ ┴
src └─┘ └─┘
typ ┴ ┴ └─┘ └─┘ ┴
doc └──┘
636 preimage f (⋃₀ s) = (⋃t ∈ s, preimage f t) :=
id └──────┘ ┴ └┘ ┴ ┴ ┴┴ ┴┴ └──────┘ ┴ ┴
src └──────┘ └┘ ┴ ┴ ┴ └──────┘
typ └──────┘ ┴ └┘ ┴ ┴ ┴┴ ┴┴ └──────┘ ┴ ┴
doc └──────┘ ┴ ┴ └──────┘
637 set.ext $ by simp [preimage]
id └─────┘ └──────┘
src └─────┘ └────┘└──────┘└─
typ └─────┘ └────┘└──────┘└─
doc └────┘└──────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────
638
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
639 lemma preimage_Inter {ι : Sort*} {s : ι → set β} {f : α → β} :
id ┴ └─┘ ┴ ┴ ┴
src └─┘
typ ┴ └─┘ ┴ ┴ ┴
640 f ⁻¹' (⋂ i, s i) = (⋂ i, f ⁻¹' s i) :=
id ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴
doc └─┘ ┴ ┴ ┴ ┴ └─┘
641 by ext; simp
src └─┘ └────
typ └─┘ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid └
st └──────────
642
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
643 lemma preimage_bInter {s : γ → set β} {t : set γ} {f : α → β} :
id ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
644 f ⁻¹' (⋂ i∈t, s i) = (⋂ i∈t, f ⁻¹' s i) :=
id ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴
doc └─┘ ┴ ┴ ┴ ┴ └─┘
645 by ext; simp
src └─┘ └────
typ └─┘ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid └
st └──────────
646
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
647 end preimage
648
649
650 section seq
651
652 def seq (s : set (α → β)) (t : set α) : set β := {b | ∃f∈s, ∃a∈t, (f : α → β) a = b}
id └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴┴ ┴┴ ┴┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴┴ ┴┴ ┴┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
653
654 lemma seq_def {s : set (α → β)} {t : set α} : seq s t = ⋃f∈s, f '' t :=
id └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ └┘ ┴
src └─┘ └─┘ └─┘ ┴ ┴ ┴ └┘
typ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴┴ ┴ └┘ ┴
doc ┴ ┴
655 set.ext $ by simp [seq]
id └─────┘ └─┘
src └─────┘ └────┘└─┘└─
typ └─────┘ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
656
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
657 @[simp] lemma mem_seq_iff {s : set (α → β)} {t : set α} {b : β} :
id └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴
doc └──┘
658 b ∈ seq s t ↔ ∃ (f ∈ s) (a ∈ t), (f : α → β) a = b :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
659 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
660
661 lemma seq_subset {s : set (α → β)} {t : set α} {u : set β} :
id └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴
662 seq s t ⊆ u ↔ (∀f∈s, ∀a∈t, (f : α → β) a ∈ u) :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
663 iff.intro
id └───────┘
src └───────┘
typ └───────┘
664 (assume h f hf a ha, h ⟨f, hf, a, ha, rfl⟩)
id ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └─┘
src └─┘
typ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ └─┘
665 (assume h b ⟨f, hf, a, ha, eq⟩, eq ▸ h f hf a ha)
id ┴ ┴ ┴┴ └┘ ┴ └┘ └┘ ┴ ┴
src └┘ ┴
typ ┴ ┴ ┴┴ └┘ ┴ └┘ └┘ ┴ ┴
666
667 lemma seq_mono {s₀ s₁ : set (α → β)} {t₀ t₁ : set α} (hs : s₀ ⊆ s₁) (ht : t₀ ⊆ t₁) :
id └─┘ ┴ ┴ └─┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
src └─┘ └─┘ ┴ ┴
typ └─┘ ┴ ┴ └─┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
668 seq s₀ t₀ ⊆ seq s₁ t₁ :=
id └─┘ └┘ └┘ ┴ └─┘ └┘ └┘
src └─┘ ┴ └─┘
typ └─┘ └┘ └┘ ┴ └─┘ └┘ └┘
669 assume b ⟨f, hf, a, ha, eq⟩, ⟨f, hs hf, a, ht ha, eq⟩
id ┴ ┴┴ └┘ ┴ └┘ └┘ └┘ └┘
src └┘
typ ┴ ┴┴ └┘ ┴ └┘ └┘ └┘ └┘
670
671 lemma singleton_seq {f : α → β} {t : set α} : set.seq {f} t = f '' t :=
id ┴ ┴ └─┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴ └┘ ┴
src └─┘ └─────┘ ┴ ┴ └┘
typ ┴ ┴ └─┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴ └┘ ┴
672 set.ext $ by simp
id └─────┘
src └─────┘ └────
typ └─────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
673
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
674 lemma seq_singleton {s : set (α → β)} {a : α} : set.seq s {a} = (λf:α→β, f a) '' s :=
id └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴ └┘ ┴
src └─┘ └─────┘ ┴ ┴ └┘
typ └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴ └┘ ┴
675 set.ext $ by simp
id └─────┘
src └─────┘ └────
typ └─────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
676
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
677 lemma seq_seq {s : set (β → γ)} {t : set (α → β)} {u : set α} :
id └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
678 seq s (seq t u) = seq (seq ((∘) '' s) t) u :=
id └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴
src └─┘ └─┘ ┴ └─┘ └─┘ ┴ └┘
typ └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴
679 begin
st └─────
680 refine set.ext (assume c, iff.intro _ _),
id └─────┘ └───────┘
src └─────┘└─────┘┴ └──┘└───────┘└───┘
typ └─────┘└─────┘┴ └──┘└───────┘└───┘
doc └─────┘ ┴ └──┘ └───┘
txt └─────┘ ┴ └──┘ └───┘
par └─────┘ ┴ └──┘ └───┘
pid ┴ ┴ └──┘ └───┘
st ─────────────────────────────────────────┘└─
681 { rintros ⟨f, hfs, b, ⟨g, hg, a, hau, rfl⟩, rfl⟩,
src └────────────────────────────────────────────┘
typ └────────────────────────────────────────────┘
doc └────────────────────────────────────────────┘
txt └────────────────────────────────────────────┘
par └────────────────────────────────────────────┘
pid └─────────────────────────────────────┘
st ───┘└────────────────────────────────────────────┘└─
682 exact ⟨f ∘ g, ⟨(∘) f, mem_image_of_mem _ hfs, g, hg, rfl⟩, a, hau, rfl⟩ },
id ┴ ┴ └──────────────┘ └─┘ ┴ └┘ ┴ └─┘ └─┘
src └────┘ ┴┴┴ └┘ └─┘ └┘└──────────────┘└─┘ └┘ └┘ └┘ └─┘ └┘ └┘└─┘└┘
typ └────┘ ┴┴┴ └┘ └─┘┴└┘└──────────────┘└─┘└─┘└┘┴└┘└┘└┘ └─┘┴└┘└─┘└┘└─┘└┘
doc └────┘ ┴ ┴ └┘ └─┘ └┘ └─┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘
txt └────┘ ┴ ┴ └┘ └─┘ └┘ └─┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘
par └────┘ ┴ ┴ └┘ └─┘ └┘ └─┘ └┘ └┘ └┘ └─┘ └┘ └┘ └┘
pid ┴ ┴ ┴ └┘ └─┘ └┘ └─┘ └┘ └┘ └┘ └─┘ └┘ └┘ ┴┴
st ───────────────────────────────────────────────────────────────────────────┘└┘└
683 { rintros ⟨fg, ⟨fc, ⟨f, hfs, rfl⟩, g, hgt, rfl⟩, a, ha, rfl⟩,
src └────────────────────────────────────────────────────────┘
typ └────────────────────────────────────────────────────────┘
doc └────────────────────────────────────────────────────────┘
txt └────────────────────────────────────────────────────────┘
par └────────────────────────────────────────────────────────┘
pid └─────────────────────────────────────────────────┘
st ─────────────────────────────────────────────────────────────┘└─
684 exact ⟨f, hfs, g a, ⟨g, hgt, a, ha, rfl⟩, rfl⟩ }
id ┴ └─┘ ┴ └─┘ ┴ └┘ └─┘
src └────┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └─┘└─┘└┘
typ └────┘ ┴└┘└─┘└┘ ┴ └┘ ┴└┘└─┘└┘┴└┘└┘└┘ └─┘└─┘└┘
doc └────┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └─┘ └┘
txt └────┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └─┘ └┘
par └────┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └─┘ └┘
pid ┴ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └─┘ ┴┴
st ──────────────────────────────────────────────────┘└─
685 end
st ──┘
686
687 lemma image_seq {f : β → γ} {s : set (α → β)} {t : set α} :
id ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
688 f '' seq s t = seq ((∘) f '' s) t :=
id ┴ └┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴
src └┘ └─┘ ┴ └─┘ ┴ └┘
typ ┴ └┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴
689 by rw [← singleton_seq, ← singleton_seq, seq_seq, image_singleton]
id └───────────┘ └───────────┘ └─────┘ └─────────────┘
src └────┘└───────────┘└──┘└───────────┘└┘└─────┘└┘└─────────────┘└─
typ └────┘└───────────┘└──┘└───────────┘└┘└─────┘└┘└─────────────┘└─
doc └────┘ └──┘ └┘ └┘ └─
txt └────┘ └──┘ └┘ └┘ └─
par └────┘ └──┘ └┘ └┘ └─
pid └──┘ └──┘ └┘ └┘ ┴└
st └──────────────────┘└───────────────┘└───────┘└───────────────┘┴└
690
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
691 lemma prod_eq_seq {s : set α} {t : set β} : set.prod s t = (prod.mk '' s).seq t :=
id └─┘ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴ └─────┘ └┘ ┴ └─┘ ┴
src └─┘ └─┘ └──────┘ ┴ └─────┘ └┘ └─┘
typ └─┘ ┴ └─┘ ┴ └──────┘ ┴ ┴ ┴ └─────┘ └┘ ┴ └─┘ ┴
doc └──────┘
692 begin
st └─────
693 ext ⟨a, b⟩,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └─────┘
st ───────────┘└─
694 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
695 { rintros ⟨ha, hb⟩, exact ⟨prod.mk a, ⟨a, ha, rfl⟩, b, hb, rfl⟩ },
id └─────┘ ┴ └┘ ┴ └┘ └─┘
src └──────────────┘ └────┘ └─────┘┴ └┘ └┘ └┘ └─┘ └┘ └┘└─┘└┘
typ └──────────────┘ └────┘ └─────┘┴ └┘ ┴└┘└┘└┘ └─┘┴└┘└┘└┘└─┘└┘
doc └──────────────┘ └────┘ ┴ └┘ └┘ └┘ └─┘ └┘ └┘ └┘
txt └──────────────┘ └────┘ ┴ └┘ └┘ └┘ └─┘ └┘ └┘ └┘
par └──────────────┘ └────┘ ┴ └┘ └┘ └┘ └─┘ └┘ └┘ └┘
pid └───────┘ ┴ ┴ └┘ └┘ └┘ └─┘ └┘ └┘ ┴┴
st ───┘└──────────────┘└────────────────────────────────────────────┘└┘└
696 { rintros ⟨f, ⟨x, hx, rfl⟩, y, hy, eq⟩, rw ← eq, exact ⟨hx, hy⟩ }
id └┘ └┘ └┘
src └──────────────────────────────────┘ └───┘└┘ └────┘ └┘ └┘
typ └──────────────────────────────────┘ └───┘└┘ └────┘ └┘└┘└┘└┘
doc └──────────────────────────────────┘ └───┘ └────┘ └┘ └┘
txt └──────────────────────────────────┘ └───┘ └────┘ └┘ └┘
par └──────────────────────────────────┘ └───┘ └────┘ └┘ └┘
pid └───────────────────────────┘ └─┘ ┴ └┘ ┴┴
st ───────────────────────────────────────┘└───────┘└───────────────┘└─
697 end
st ──┘
698
699 lemma prod_image_seq_comm (s : set α) (t : set β) :
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
700 (prod.mk '' s).seq t = seq ((λb a, (a, b)) '' t) s :=
id └─────┘ └┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴
src └─────┘ └┘ └─┘ ┴ └─┘ ┴ └┘
typ └─────┘ └┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴
701 by rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]
id └─────────┘ └─────────────┘ └─────────┘ └───────┘ └────────┘
src └────┘└─────────┘└──┘└─────────────┘└┘└─────────┘└┘└───────┘└──┘└────────┘└─
typ └────┘└─────────┘└──┘└─────────────┘└┘└─────────┘└┘└───────┘└──┘└────────┘└─
doc └────┘ └──┘ └┘ └┘ └──┘ └─
txt └────┘ └──┘ └┘ └┘ └──┘ └─
par └────┘ └──┘ └┘ └┘ └──┘ └─
pid └──┘ └──┘ └┘ └┘ └──┘ ┴└
st └────────────────┘└─────────────────┘└───────────┘└─────────┘└────────────┘┴└
702
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
703 end seq
704
705 theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ}
id └──────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └──────┘ └─┘ └─┘
typ └──────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
706 (hf : monotone f) (hg : monotone g) : monotone (λx, set.prod (f x) (g x)) :=
id └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──────┘ └──────┘ └──────┘ └──────┘
typ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘ └──────┘
707 assume a b h, prod_mono (hf h) (hg h)
id ┴ ┴ ┴ └───────┘ └┘ ┴ └┘ ┴
src └───────┘
typ ┴ ┴ ┴ └───────┘ └┘ ┴ └┘ ┴
708
709 instance : monad set :=
id └───┘ └─┘
src └───┘ └─┘
typ └───┘ └─┘
710 { pure := λ(α : Type u) a, {a},
id └──┘ ┴ ┴┴
src ┴
typ └──┘ ┴ ┴┴
711 bind := λ(α β : Type u) s f, ⋃i∈s, f i,
id └──┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src ┴ ┴
typ └──┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc ┴ ┴
712 seq := λ(α β : Type u), set.seq,
id └──┘ └─────┘
src └─────┘
typ └──┘ └─────┘
713 map := λ(α β : Type u), set.image }
id └──┘ └───────┘
src └───────┘
typ └──┘ └───────┘
714
715 instance : is_lawful_monad set :=
id └─────────────┘ └─┘
src └─────────────┘ └─┘
typ └─────────────┘ └─┘
716 { pure_bind := assume α β x f, by simp,
id ┴ ┴ ┴ ┴ ┴
src ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
717 bind_assoc := assume α β γ s f g, set.ext $ assume a,
id ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
718 by simp [exists_and_distrib_right.symm, -exists_and_distrib_right,
src └────┘ └────────────────────────────
typ └────┘└───────────────────────────┘└────────────────────────────
doc └────┘ └────────────────────────────
txt └────┘ └────────────────────────────
par └────┘ └────────────────────────────
pid ┴┴ └────────────────────────────
st └────────────────────────────────────────────────────────────────
719 exists_and_distrib_left.symm, -exists_and_distrib_left, and_assoc];
id └───────┘
src ────────────┘ └──────────────────────────┘└───────┘┴
typ ────────────┘└──────────────────────────┘└──────────────────────────┘└───────┘┴
doc ────────────┘ └──────────────────────────┘ ┴
txt ────────────┘ └──────────────────────────┘ ┴
par ────────────┘ └──────────────────────────┘ ┴
pid ────────────┘ └──────────────────────────┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────
720 exact exists_swap,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘
721 id_map := assume α, id_map,
id ┴ └────┘
src └────┘
typ ┴ └────┘
722 bind_pure_comp_eq_map := assume α β f s, set.ext $ by simp [set.image, eq_comm],
id ┴ ┴ ┴ ┴ └─────┘ └───────┘ └─────┘
src └─────┘ └────┘└───────┘└┘└─────┘┴
typ ┴ ┴ ┴ ┴ └─────┘ └────┘└───────┘└┘└─────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └────────────────────────┘
723 bind_map_eq_seq := assume α β s t, by simp [seq_def] }
id ┴ ┴ ┴ ┴ └─────┘
src └────┘└─────┘└┘
typ ┴ ┴ ┴ ┴ └────┘└─────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └──────────────┘
724
725 instance : is_comm_applicative (set : Type u → Type u) :=
id └─────────────────┘ └─┘ └──┘
src └─────────────────┘ └─┘
typ └─────────────────┘ └─┘ └──┘
726 ⟨ assume α β s t, prod_image_seq_comm s t ⟩
id ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
src └─────────────────┘
typ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
727
728 section monad
729 variables {α' β' : Type u} {s : set α'} {f : α' → set β'} {g : set (α' → β')}
id └─┘ └─┘ └─┘
src └─┘ └─┘ └─┘
typ └─┘ └─┘ └─┘
730
731 @[simp] lemma bind_def : s >>= f = ⋃i∈s, f i := rfl
id ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └─┘
src └─┘ ┴ ┴ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ └─┘
doc └──┘ ┴ ┴
732
733 @[simp] lemma fmap_eq_image (f : α' → β') : f <$> s = f '' s := rfl
id └┘ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └─┘ ┴ └┘ └─┘
typ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──┘
734
735 @[simp] lemma seq_eq_set_seq {α β : Type*} (s : set (α → β)) (t : set α) : s <*> t = s.seq t := rfl
id └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ └─┘
src └─┘ └─┘ └─┘ ┴ └──┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ └─┘
doc └──┘
736
737 @[simp] lemma pure_def (a : α) : (pure a : set α) = {a} := rfl
id ┴ └──┘ ┴ └─┘ ┴ ┴ ┴┴ └─┘
src └──┘ └─┘ ┴ ┴ └─┘
typ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴┴ └─┘
doc └──┘
738
739 end monad
740
741 section pi
742
743 lemma pi_def {α : Type*} {π : α → Type*} (i : set α) (s : Πa, set (π a)) :
id ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴
744 pi i s = (⋂ a∈i, ((λf:(Πa, π a), f a) ⁻¹' (s a))) :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └┘ ┴ ┴ ┴ └─┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
doc └┘ ┴ ┴ └─┘
745 by ext; simp [pi]
id └┘
src └─┘ └────┘└┘└─
typ └─┘ └────┘└┘└─
doc └─┘ └────┘└┘└─
txt └─┘ └────┘ └─
par └─┘ └────┘ └─
pid ┴┴ ┴└
st └───────────────
746
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
747 end pi
748
749 end set
750
751 /- disjoint sets -/
752
753 section disjoint
754 variable [semilattice_inf_bot α]
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
755
756 /-- Two elements of a lattice are disjoint if their inf is the bottom element.
757 (This generalizes disjoint sets, viewed as members of the subset lattice.) -/
758 def disjoint (a b : α) : Prop := a ⊓ b ≤ ⊥
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
759
760 theorem disjoint.eq_bot {a b : α} (h : disjoint a b) : a ⊓ b = ⊥ :=
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴
typ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘
761 eq_bot_iff.2 h
id └────────┘┴ ┴
src └────────┘┴
typ └────────┘┴ ┴
762
763 theorem disjoint_iff {a b : α} : disjoint a b ↔ a ⊓ b = ⊥ :=
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴
typ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘
764 eq_bot_iff.symm
id └────────┘└───┘
src └────────┘└───┘
typ └────────┘└───┘
765
766 theorem disjoint.comm {a b : α} : disjoint a b ↔ disjoint b a :=
id ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ ┴ └──────┘
typ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
767 by rw [disjoint, disjoint, inf_comm]
id └──────┘ └──────┘ └──────┘
src └──┘└──────┘└┘└──────┘└┘└──────┘└─
typ └──┘└──────┘└┘└──────┘└┘└──────┘└─
doc └──┘└──────┘└┘└──────┘└┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └───────────┘└────────┘└────────┘┴└
768
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
769 theorem disjoint.symm {a b : α} : disjoint a b → disjoint b a :=
id ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ └──────┘
typ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
770 disjoint.comm.1
id └───────────┘┴
src └───────────┘┴
typ └───────────┘┴
771
772 @[simp] theorem disjoint_bot_left {a : α} : disjoint ⊥ a := disjoint_iff.2 bot_inf_eq
id ┴ └──────┘ ┴ ┴ └──────────┘┴ └────────┘
src └──────┘ ┴ └──────────┘┴ └────────┘
typ ┴ └──────┘ ┴ ┴ └──────────┘┴ └────────┘
doc └──┘ └──────┘
773 @[simp] theorem disjoint_bot_right {a : α} : disjoint a ⊥ := disjoint_iff.2 inf_bot_eq
id ┴ └──────┘ ┴ ┴ └──────────┘┴ └────────┘
src └──────┘ ┴ └──────────┘┴ └────────┘
typ ┴ └──────┘ ┴ ┴ └──────────┘┴ └────────┘
doc └──┘ └──────┘
774
775 theorem disjoint_mono {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
776 disjoint b d → disjoint a c := le_trans (inf_le_inf h₁ h₂)
id └──────┘ ┴ ┴ └──────┘ ┴ ┴ └──────┘ └────────┘ └┘ └┘
src └──────┘ └──────┘ └──────┘ └────────┘
typ └──────┘ ┴ ┴ └──────┘ ┴ ┴ └──────┘ └────────┘ └┘ └┘
doc └──────┘ └──────┘
777
778 theorem disjoint_mono_left {a b c : α} (h : a ≤ b) : disjoint b c → disjoint a c :=
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src ┴ └──────┘ └──────┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
779 disjoint_mono h (le_refl _)
id └───────────┘ ┴ └─────┘
src └───────────┘ └─────┘
typ └───────────┘ ┴ └─────┘
780
781 theorem disjoint_mono_right {a b c : α} (h : b ≤ c) : disjoint a c → disjoint a b :=
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
src ┴ └──────┘ └──────┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
782 disjoint_mono (le_refl _) h
id └───────────┘ └─────┘ ┴
src └───────────┘ └─────┘
typ └───────────┘ └─────┘ ┴
783
784 @[simp] lemma disjoint_self {a : α} : disjoint a a ↔ a = ⊥ :=
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ ┴
typ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──────┘
785 by simp [disjoint]
id └──────┘
src └────┘└──────┘└─
typ └────┘└──────┘└─
doc └────┘└──────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────
786
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
787 lemma ne_of_disjoint {a b : α} (ha : a ≠ ⊥) (hab : disjoint a b) : a ≠ b :=
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘
788 by { intro h, rw [←h, disjoint_self] at hab, exact ha hab }
id ┴ └───────────┘ └┘ └─┘
src └─────┘ └───┘ └┘└───────────┘└──────┘ └────┘ ┴ ┴
typ └─────┘ └───┘┴└┘└───────────┘└──────┘ └────┘└┘┴└─┘┴
doc └─────┘ └───┘ └┘ └──────┘ └────┘ ┴ ┴
txt └─────┘ └───┘ └┘ └──────┘ └────┘ ┴ ┴
par └─────┘ └───┘ └┘ └──────┘ └────┘ ┴ ┴
pid └┘ └─┘ └┘ ┴└─────┘ ┴ ┴ ┴
st └────────┘└──────┘└─────────────┘┴└─────┘└─────────────┘└┘
789
790 end disjoint
791
792 namespace set
793
794 protected theorem disjoint_iff {s t : set α} : disjoint s t ↔ s ∩ t ⊆ ∅ := iff.rfl
id └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
src └─┘ └──────┘ ┴ ┴ ┴ ┴ └─────┘
typ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──────┘
795
796 lemma not_disjoint_iff {s t : set α} : ¬disjoint s t ↔ ∃x, x ∈ s ∧ x ∈ t :=
id └─┘ ┴ ┴└──────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴└──────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴└──────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘
797 (not_congr (set.disjoint_iff.trans subset_empty_iff)).trans ne_empty_iff_nonempty
id └───────┘ └──────────────┘└────┘ └──────────────┘ └───┘ └───────────────────┘
src └───────┘ └──────────────┘└────┘ └──────────────┘ └───┘ └───────────────────┘
typ └───────┘ └──────────────┘└────┘ └──────────────┘ └───┘ └───────────────────┘
798
799 lemma disjoint_left {s t : set α} : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
id └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └──────┘ ┴ ┴ ┴
typ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘
800 show (∀ x, ¬(x ∈ s ∩ t)) ↔ _, from ⟨λ h a, not_and.1 $ h a, λ h a, not_and.2 $ h a⟩
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘┴ ┴ ┴ ┴ ┴ └─────┘┴ ┴ ┴
src ┴ ┴ ┴ ┴ └─────┘┴ └─────┘┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘┴ ┴ ┴ ┴ ┴ └─────┘┴ ┴ ┴
801
802 theorem disjoint_right {s t : set α} : disjoint s t ↔ ∀ {a}, a ∈ t → a ∉ s :=
id └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └──────┘ ┴ ┴ ┴
typ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘
803 by rw [disjoint.comm, disjoint_left]
id └───────────┘ └───────────┘
src └──┘└───────────┘└┘└───────────┘└─
typ └──┘└───────────┘└┘└───────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────────┘└─────────────┘┴└
804
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
805 theorem disjoint_diff {a b : set α} : disjoint a (b \ a) :=
id └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴
src └─┘ └──────┘ ┴
typ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──────┘
806 disjoint_iff.2 (inter_diff_self _ _)
id └──────────┘┴ └─────────────┘
src └──────────┘┴ └─────────────┘
typ └──────────┘┴ └─────────────┘
807
808 theorem disjoint_compl (s : set α) : disjoint s (-s) := assume a ⟨h₁, h₂⟩, h₂ h₁
id └─┘ ┴ └──────┘ ┴ ┴┴ ┴ ┴└┘ └┘
src └─┘ └──────┘ ┴
typ └─┘ ┴ └──────┘ ┴ ┴┴ ┴ ┴└┘ └┘
doc └──────┘
809
810 theorem disjoint_singleton_left {a : α} {s : set α} : disjoint {a} s ↔ a ∉ s :=
id ┴ └─┘ ┴ └──────┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └──────┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ └──────┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘
811 by simp [set.disjoint_iff, subset_def]; exact iff.rfl
id └──────────────┘ └────────┘ └─────┘
src └────┘└──────────────┘└┘└────────┘┴ └────┘└─────┘└
typ └────┘└──────────────┘└┘└────────┘┴ └────┘└─────┘└
doc └────┘ └┘ ┴ └────┘ └
txt └────┘ └┘ ┴ └────┘ └
par └────┘ └┘ ┴ └────┘ └
pid ┴┴ └┘ ┴ ┴ └
st └───────────────────────────────────────────────────
812
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
813 theorem disjoint_singleton_right {a : α} {s : set α} : disjoint s {a} ↔ a ∉ s :=
id ┴ └─┘ ┴ └──────┘ ┴ ┴┴ ┴ ┴ ┴ ┴
src └─┘ └──────┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ └──────┘ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └──────┘
814 by rw [disjoint.comm]; exact disjoint_singleton_left
id └───────────┘ └─────────────────────┘
src └──┘└───────────┘┴ └────┘└─────────────────────┘└
typ └──┘└───────────┘┴ └────┘└─────────────────────┘└
doc └──┘ ┴ └────┘ └
txt └──┘ ┴ └────┘ └
par └──┘ ┴ └────┘ └
pid └┘ ┴ ┴ └
st └────────────────┘┴└───────────────────────────────
815
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
816 theorem disjoint_image_image {f : β → α} {g : γ → α} {s : set β} {t : set γ}
id ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴
817 (h : ∀b∈s, ∀c∈t, f b ≠ g c) : disjoint (f '' s) (g '' t) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ └──────┘ └┘ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ ┴ └┘ ┴
doc └──────┘
818 by rintros a ⟨⟨b, hb, eq⟩, ⟨c, hc, rfl⟩⟩; exact h b hb c hc eq
id ┴ ┴ └┘ ┴ └┘ └┘
src └───────────────────────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴└┘└
typ └───────────────────────────────────┘ └────┘┴┴┴┴└┘┴┴┴└┘┴└┘└
doc └───────────────────────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └
txt └───────────────────────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └
par └───────────────────────────────────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └
pid └────────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────────
819
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
820 def pairwise_disjoint (s : set (set α)) : Prop :=
id └─┘ └─┘ ┴
src └─┘ └─┘
typ └─┘ └─┘ ┴
821 pairwise_on s disjoint
id └─────────┘ ┴ └──────┘
src └─────────┘ └──────┘
typ └─────────┘ ┴ └──────┘
doc └─────────┘ └──────┘
822
823 lemma pairwise_disjoint_subset {s t : set (set α)} (h : s ⊆ t)
id └─┘ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴
typ └─┘ └─┘ ┴ ┴ ┴ ┴
824 (ht : pairwise_disjoint t) : pairwise_disjoint s :=
id └───────────────┘ ┴ └───────────────┘ ┴
src └───────────────┘ └───────────────┘
typ └───────────────┘ ┴ └───────────────┘ ┴
825 pairwise_on.mono h ht
id └──────────────┘ ┴ └┘
src └──────────────┘
typ └──────────────┘ ┴ └┘
826
827 lemma pairwise_disjoint_range {s : set (set α)} (f : s → set α) (hf : ∀(x : s), f x ⊆ x.1)
id └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴
src └─┘ └─┘ └─┘ ┴ ┴
typ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴┴
828 (ht : pairwise_disjoint s) : pairwise_disjoint (range f) :=
id └───────────────┘ ┴ └───────────────┘ └───┘ ┴
src └───────────────┘ └───────────────┘ └───┘
typ └───────────────┘ ┴ └───────────────┘ └───┘ ┴
doc └───┘
829 begin
st └─────
830 rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy, refine disjoint_mono (hf x) (hf y) (ht _ x.2 _ y.2 _),
id └───────────┘ └┘ └┘ ┴ ┴
src └──────────────────────────────┘ └─────┘└───────────┘┴ ┴ └┘ ┴ └┘ └─┘ └───┘ └───┘
typ └──────────────────────────────┘ └─────┘└───────────┘┴ ┴ └┘ └┘┴ └┘ └┘└─┘┴└───┘┴└───┘
doc └──────────────────────────────┘ └─────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └───┘ └───┘
txt └──────────────────────────────┘ └─────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └───┘ └───┘
par └──────────────────────────────┘ └─────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └───┘ └───┘
pid └────────────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ └───┘ └───┘
st ─────────────────────────────────┘└─────────────────────────────────────────────────────┘└─
831 intro h, apply hxy, apply congr_arg f, exact subtype.eq h
id └───────┘ ┴ └────────┘ ┴
src └─────┘ └────┘ └────┘└───────┘┴ └────┘└────────┘┴ ┴
typ └─────┘ └────┘ └────┘└───────┘┴┴ └────┘└────────┘┴┴┴
doc └─────┘ └────┘ └────┘ ┴ └────┘ ┴ ┴
txt └─────┘ └────┘ └────┘ ┴ └────┘ ┴ ┴
par └─────┘ └────┘ └────┘ ┴ └────┘ ┴ ┴
pid └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ────────┘└─────────┘└─────────────────┘└───────────────────┘
832 end
st └─┘
833
834 /- warning: classical -/
835 lemma pairwise_disjoint_elim {s : set (set α)} (h : pairwise_disjoint s) {x y : set α}
id └─┘ └─┘ ┴ └───────────────┘ ┴ └─┘ ┴
src └─┘ └─┘ └───────────────┘ └─┘
typ └─┘ └─┘ ┴ └───────────────┘ ┴ └─┘ ┴
836 (hx : x ∈ s) (hy : y ∈ s) (z : α) (hzx : z ∈ x) (hzy : z ∈ y) : x = y :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
837 classical.not_not.1 $ λ h', h x hx y hy h' ⟨hzx, hzy⟩
id └───────────────┘┴ └┘ ┴ ┴ └┘ ┴ └┘ └┘ └─┘ └─┘
src └───────────────┘┴
typ └───────────────┘┴ └┘ ┴ ┴ └┘ ┴ └┘ └┘ └─┘ └─┘
838
839 end set
840
841 namespace set
842 variables (t : α → set β)
id └─┘
src └─┘
typ └─┘
843
844 def sigma_to_Union (x : Σi, t i) : (⋃i, t i) := ⟨x.2, mem_Union.2 ⟨x.1, x.2.2⟩⟩
id ┴┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴ └───────┘┴ ┴┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────┘┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴ └───────┘┴ ┴┴ ┴┴ ┴
doc ┴ ┴
845
846 lemma surjective_sigma_to_Union : surjective (sigma_to_Union t)
id └────────┘ └────────────┘ ┴
src └────────┘ └────────────┘
typ └────────┘ └────────────┘ ┴
847 | ⟨b, hb⟩ := have ∃a, b ∈ t a, by simpa using hb, let ⟨a, hb⟩ := this in ⟨⟨a, ⟨b, hb⟩⟩, rfl⟩
id ┴ ┴┴┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘ └──┘ └─┘
src ┴ ┴ ┴ └──────────┘ └─┘
typ ┴ ┴┴┴ ┴ ┴ ┴ └──────────┘└┘ └─┘ ┴ └┘ └──┘ └─┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └─────────────┘
848
849 lemma injective_sigma_to_Union (h : ∀i j, i ≠ j → disjoint (t i) (t j)) :
id ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──────┘
850 injective (sigma_to_Union t)
id └───────┘ └────────────┘ ┴
src └───────┘ └────────────┘
typ └───────┘ └────────────┘ ┴
851 | ⟨a₁, ⟨b₁, h₁⟩⟩ ⟨a₂, ⟨b₂, h₂⟩⟩ eq :=
id └┘ └┘ └┘ └┘ └┘ └┘ └┘
src └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └┘
852 have b_eq : b₁ = b₂, from congr_arg subtype.val eq,
id ┴ └───────┘ └─────────┘
src ┴ └───────┘ └─────────┘
typ ┴ └───────┘ └─────────┘
853 have a_eq : a₁ = a₂, from classical.by_contradiction $ assume ne,
id ┴ └────────────────────────┘ └┘
src ┴ └────────────────────────┘ └┘
typ ┴ └────────────────────────┘ └┘
854 have b₁ ∈ t a₁ ∩ t a₂, from ⟨h₁, b_eq.symm ▸ h₂⟩,
id ┴ ┴ ┴ ┴ └──┘└───┘ ┴
src ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ └──┘└───┘ ┴
855 h _ _ ne this,
id ┴ └┘ └──┘
src └┘
typ ┴ └┘ └──┘
856 sigma.eq a_eq $ subtype.eq $ by subst b_eq; subst a_eq
id └──────┘ └──┘ └────────┘ └──┘ └──┘
src └──────┘ └────────┘ └────┘ └────┘ └
typ └──────┘ └──┘ └────────┘ └────┘└──┘ └────┘└──┘└
doc └────┘ └────┘ └
txt └────┘ └────┘ └
par └────┘ └────┘ └
pid ┴ ┴ └
st └───────────────────────
857
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
858 lemma bijective_sigma_to_Union (h : ∀i j, i ≠ j → disjoint (t i) (t j)) :
id ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──────┘
859 bijective (sigma_to_Union t) :=
id └───────┘ └────────────┘ ┴
src └───────┘ └────────────┘
typ └───────┘ └────────────┘ ┴
860 ⟨injective_sigma_to_Union t h, surjective_sigma_to_Union t⟩
id └──────────────────────┘ ┴ ┴ └───────────────────────┘ ┴
src └──────────────────────┘ └───────────────────────┘
typ └──────────────────────┘ ┴ ┴ └───────────────────────┘ ┴
861
862 noncomputable def Union_eq_sigma_of_disjoint {t : α → set β}
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
863 (h : ∀i j, i ≠ j → disjoint (t i) (t j)) : (⋃i, t i) ≃ (Σi, t i) :=
id ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc └──────┘ ┴ ┴ ┴
864 (equiv.of_bijective $ bijective_sigma_to_Union t h).symm
id └────────────────┘ └──────────────────────┘ ┴ ┴ └──┘
src └────────────────┘ └──────────────────────┘ └──┘
typ └────────────────┘ └──────────────────────┘ ┴ ┴ └──┘
865
866 noncomputable def bUnion_eq_sigma_of_disjoint {s : set α} {t : α → set β}
id └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ ┴ └─┘ ┴
867 (h : pairwise_on s (disjoint on t)) : (⋃i∈s, t i) ≃ (Σi:s, t i.val) :=
id └─────────┘ ┴ └──────┘ └┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴└──┘
src └─────────┘ └──────┘ └┘ ┴ ┴ ┴ ┴ ┴ └──┘
typ └─────────┘ ┴ └──────┘ └┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴└──┘
doc └─────────┘ └──────┘ ┴ ┴ ┴
868 equiv.trans (equiv.set_congr (bUnion_eq_Union _ _)) $ Union_eq_sigma_of_disjoint $
id └─────────┘ └─────────────┘ └─────────────┘ └────────────────────────┘
src └─────────┘ └─────────────┘ └─────────────┘ └────────────────────────┘
typ └─────────┘ └─────────────┘ └─────────────┘ └────────────────────────┘
869 assume ⟨i, hi⟩ ⟨j, hj⟩ ne, h _ hi _ hj $ assume eq, ne $ subtype.eq eq
id ┴ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └────────┘ └┘
src └┘ └┘ └┘ └────────┘ └┘
typ ┴ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └────────┘ └┘
870
871 end set